exact ⟨mem_maximalConsistentTheory_iff.mpr (by prover [this]),
       mem_maximalConsistentTheory_iff.mpr (by prover [this])⟩
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
no goals