intros P h₁
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication (↑t) (lindenbaumExtension u Δ) ⊆ ↑↑p
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
⊢ P ∈ ↑↑p