We will prove S_Omega ⊆ Sbar_Omega.

An exact proof term for the current goal is (binunion_Subq_1 S_Omega {S_Omega}).

∎