Theorem: LO.Propositional.Classical.satisfiable_of_consistent (Logic/Propositional/Classical/Basic/Completeness.lean)

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT✝ consisT : Consistent T
⊢ T ⊆ maximalConsistentTheory consisT
Tactic:
simp
State after:
no goals