simp
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ ⋃₀ c ∈ {U | Consistent U}
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
⊢ Consistent (⋃₀ c)