have ⟨Q,h₂,h₃⟩ := h₁
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
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 Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ P ∈ ↑↑p