have l₃ : isDisjunctionClosed Δ := by
  intros P Q h₁ h₂
  have ⟨R,l₄⟩ := nonconstruction h₁.left
  have ⟨⟨S,⟨prf₁⟩,l₆⟩,l₈⟩ := nonconstruction l₄
  have ⟨T,l₉⟩ := nonconstruction h₁.right
  have ⟨⟨U,⟨prf₂⟩,l₁₀⟩,l₁₂⟩ := nonconstruction l₉
  clear h₁ l₄ l₉
  have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
  apply l₁₃
  apply h₂
  clear l₈ l₁₂ l₁₃ h₂
  have l₁₄ : S¦U ∈ ▲{P¦Q} := ⟨(BTheorem.orFunctor prf₁.toTheorem prf₂.toTheorem).toProof⟩
  have l₁₅ : (S¦U ⊃ R¦T) ∈ t := t.property.mpr ⟨BProof.mp (BProof.adj 
    (BProof.mp (BProof.ax l₆) (BTheorem.hs BTheorem.taut BTheorem.orI₁))
    (BProof.mp (BProof.ax l₁₀) (BTheorem.hs BTheorem.taut BTheorem.orI₂)))
    BTheorem.orE⟩
  exact ⟨S ¦ U, l₁₄, l₁₅⟩
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p