obtain ⟨x, y, rxy, z, ryz, nryz, nrzy⟩ := hCon
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
hCon : ∃ x x_1, F.Rel x x_1 ∧ ∃ x_2, F.Rel x x_2 ∧ ¬F.Rel x_1 x_2 ∧ ¬F.Rel x_2 x_1
⊢ ¬F ⊧* .𝟯
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
x y : F.World
rxy : F.Rel x y
z : F.World
ryz : F.Rel x z
nryz : ¬F.Rel y z
nrzy : ¬F.Rel z y
⊢ ¬F ⊧* .𝟯