apply byContradiction
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
⊢ formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
case 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 Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p → False