We will prove TransSet S_Omega.

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).

An exact proof term for the current goal is (ordinal_TransSet S_Omega Hord).

∎