We will prove simply_ordered_set (setprod 2 ω).

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

Apply orIL to the current goal.

Apply orIL to the current goal.

Apply orIR to the current goal.

Use reflexivity.

∎