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