We will prove uncountable_set Sbar_Omega.
Assume Hcount: countable_set Sbar_Omega.
Apply FalseE to the current goal.
We prove the intermediate claim Hsub: S_Omega ⊆ Sbar_Omega.
An exact proof term for the current goal is S_Omega_Subq_Sbar_Omega.
We prove the intermediate claim HcountS: countable Sbar_Omega.
An exact proof term for the current goal is Hcount.
We prove the intermediate claim HcountSO: countable S_Omega.
An exact proof term for the current goal is (Subq_countable S_Omega Sbar_Omega HcountS Hsub).
We prove the intermediate claim HuncSO: uncountable_set S_Omega.
An exact proof term for the current goal is (andER (well_ordered_set S_Omega) (uncountable_set S_Omega) S_Omega_well_ordered_uncountable).
An exact proof term for the current goal is (HuncSO HcountSO).
∎