have ⟨q,h₂,h₃⟩ := lemma1 t u p h₁
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p