have l₂ : ↑u ∩ Δ = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros P h₂
  have l₃ : ▲{P} ⊆ ↑u := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
  have l₄ := formalAppMonotoneLeft ↑t l₃
  exact h₂.right $ le_trans l₄ h₁
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∃ 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 ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p