have := Ω.maximal (Set.ssubset_insert hC.1)
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
⊢ False
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False