intros g h₃
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
g : Form
h₃ : g ∈ generatedDisjunctions x
⊢ {g}⊢x