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

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
⊢ Consistent (theory (maximalConsistentTheory consisT))
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
⊢ maximalConsistentTheory consisT ⊆ theory (maximalConsistentTheory consisT)
Tactic:
simpa using System.Axiomatized.axm_subset (maximalConsistentTheory consisT)
State after:
no goals