We will prove well_ordered_set Sbar_Omega.
We will prove ordinal Sbar_Omega ∧ Sbar_Omega ≠ R ∧ Sbar_Omega ≠ rational_numbers ∧ Sbar_Omega ≠ setprod 2 ω ∧ Sbar_Omega ≠ setprod R R.
Set T0 to be the term ordinal Sbar_Omega ∧ Sbar_Omega ≠ R.
Set T1 to be the term T0 ∧ Sbar_Omega ≠ rational_numbers.
Set T2 to be the term T1 ∧ Sbar_Omega ≠ setprod 2 ω.
Set T3 to be the term T2 ∧ Sbar_Omega ≠ setprod R R.
We will prove T3.
Apply andI to the current goal.
We will prove T2.
Apply andI to the current goal.
We will prove T1.
Apply andI to the current goal.
We will prove T0.
Apply andI to the current goal.
An exact proof term for the current goal is Sbar_Omega_ordinal.
An exact proof term for the current goal is Sbar_Omega_neq_R.
An exact proof term for the current goal is Sbar_Omega_neq_rational_numbers.
An exact proof term for the current goal is Sbar_Omega_neq_setprod_2_omega.
An exact proof term for the current goal is Sbar_Omega_neq_setprod_R_R.
∎