intros p h₂
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ~f ∈ p