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