assumption
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
hp : p ∉ maximalConsistentTheory consisT ∧ ~p ∉ maximalConsistentTheory consisT
this✝ : Consistent (insert p (maximalConsistentTheory consisT))
this : insert p (maximalConsistentTheory consisT) ≠ maximalConsistentTheory consisT
⊢ Consistent (insert p (maximalConsistentTheory consisT))
no goals