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