exact ⟨Z, con, ss, by intro U conU ssU; simpa using hZ U conU ssU⟩
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
no goals