clear l₂ l₃
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p