clear h₁ l₄ l₉
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (▲{P}) ↑u → R ∈ ↑↑p)
S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (▲{Q}) ↑u → T ∈ ↑↑p)
U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (▲{P¦Q}) ↑u ⊆ ↑↑p
R S : Form
l₆ : S ∈ ↑u
prf₁ : BProof {P} (S⊃R)
l₈ : ¬R ∈ ↑↑p
T U : Form
l₁₀ : U ∈ ↑u
prf₂ : BProof {Q} (U⊃T)
l₁₂ : ¬T ∈ ↑↑p
⊢ False