intro X Y Z ⟨hXY, hXZ⟩
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ ∀ ⦃x y z : MCT 𝓓⦄,
    □''⁻¹x.theory ⊆ y.theory ∧ □''⁻¹x.theory ⊆ z.theory → □''⁻¹y.theory ⊆ z.theory ∨ □''⁻¹z.theory ⊆ y.theory
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
⊢ □''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory