apply Iff.intro
case a.h
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) ↔ f ∈ ↑Γ
case a.h.mp
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ

case a.h.mpr
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)