apply Set.mem_interₛ.mpr
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ t_1