. intro hnp;
  by_contra hp;
  replace hp := membership_iff.mp hp;
  replace hnp := membership_iff.mp hnp;
  have : Ω.theory *⊢[L]! ⊥ := hnp ⨀ hp;
  have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum;
  contradiction;
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ ~p ∈ Ω.theory → p ∉ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ p ∉ Ω.theory → ~p ∈ Ω.theory