We will prove simply_ordered_set S_Omega.

We will prove S_Omega = R ∨ S_Omega = rational_numbers ∨ S_Omega = ω ∨ S_Omega = ω ∖ {0} ∨ S_Omega = setprod 2 ω ∨ S_Omega = setprod R R ∨ ordinal S_Omega.

Apply orIR to the current goal.

An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).

∎