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