We will prove normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology.
Apply andI to the current goal.
We prove the intermediate claim HdefTx: SOmega_topology = order_topology S_Omega.
Use reflexivity.
rewrite the current goal using HdefTx (from left to right).
We prove the intermediate claim Hwo: well_ordered_set S_Omega.
An exact proof term for the current goal is (andEL (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).
We prove the intermediate claim Hord: ordinal S_Omega.
An exact proof term for the current goal is (andEL (ordinal S_Omega) (uncountable_set S_Omega) S_Omega_ordinal_uncountable).
We prove the intermediate claim Hso: 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 Hord.
An exact proof term for the current goal is (well_ordered_sets_normal S_Omega Hwo Hso).
We prove the intermediate claim HdefTy: SbarOmega_topology = order_topology Sbar_Omega.
Use reflexivity.
rewrite the current goal using HdefTy (from left to right).
An exact proof term for the current goal is (well_ordered_sets_normal Sbar_Omega Sbar_Omega_well_ordered_set simply_ordered_set_Sbar_Omega).
∎