obtain ⟨p, hpY, hpZ⟩ := nhYZ
α : 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
nhYZ : ∃ a ∈ □''⁻¹Y.theory, a ∉ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
⊢ False
case intro.intro
α : 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
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpY : p ∈ □''⁻¹Y.theory
hpZ : p ∉ Z.theory
⊢ False