existsi ⟨
  Ω,
  hΩ₁,
  by
    rintro U ⟨hU₁, hU₂⟩;
    by_contra hC;
    have : U = Ω := hΩ₃ U hC hU₁;
    subst_vars;
    simp at hU₂,
⟩
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∃ Ω, T ⊆ Ω.theory
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ T ⊆ { theory := Ω, consistent := ⋯, maximal := ⋯ }.theory