apply Iff.intro
case h
t : Th
x : Form
⊢ x ∈ ↑t ↔ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
case h.mp
t : Th
x : Form
⊢ x ∈ ↑t → x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

case h.mpr
t : Th
x : Form
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ ↑t