have : maximalConsistentTheory consisT ⊢! p ⋏ q := mem_maximalConsistentTheory_iff.mp h
α : 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
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT