simp only [Theory.iSigma, Theory.indH, Theory.add_def, Set.image_union, Set.union_assoc]
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐈𝚺₀ ⊆ 𝐄𝐀
L : Language
inst✝² : L.ORing
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : L.Exp
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪
      ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy 𝚺 0) ⊆
    ⇑(Semiformula.lMap Language.oringEmb) '' 𝐏𝐀⁻ ∪ (𝐄𝐗𝐏 ∪ indScheme ℒₒᵣ(exp) (Hierarchy 𝚺 0))