We will prove S_Omega ∈ Sbar_Omega.

Apply (binunionI2 S_Omega {S_Omega} S_Omega) to the current goal.

An exact proof term for the current goal is (SingI S_Omega).

∎