by_contra A
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
A : ¬(p ∈ maximalConsistentTheory consisT ∨ ~p ∈ maximalConsistentTheory consisT)
⊢ False