We will prove countable_subsets_bounded S_Omega.
We prove the intermediate claim Hex: ∃X : set, well_ordered_set X ∧ uncountable_set X ∧ countable_subsets_bounded X.
An exact proof term for the current goal is exists_uncountable_well_ordered_set.
We prove the intermediate claim Htrip: well_ordered_set S_Omega ∧ uncountable_set S_Omega ∧ countable_subsets_bounded S_Omega.
An exact proof term for the current goal is (Eps_i_ex (λX : set ⇒ well_ordered_set X ∧ uncountable_set X ∧ countable_subsets_bounded X) Hex).
An exact proof term for the current goal is (andER (well_ordered_set S_Omega ∧ uncountable_set S_Omega) (countable_subsets_bounded S_Omega) Htrip).
∎