theorem LO.Modal.Hilbert.KD5_weakerThan_KD45 {α : Type u_1} : LO.Modal.Hilbert.KD5 α ≤ₛ LO.Modal.Hilbert.KD45 α

theorem LO.Modal.Hilbert.KD5_strictlyWeakerThan_KD45 : LO.Modal.Hilbert.KD5 ℕ <ₛ LO.Modal.Hilbert.KD45 ℕ