We will prove ordinal S_Omega ∧ uncountable_set S_Omega.

Apply andI to the current goal.

An exact proof term for the current goal is (well_ordered_set_is_ordinal S_Omega (andEL (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable)).

An exact proof term for the current goal is (andER (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).

∎