Apply andI to the current goal.
We will prove atleastp ω real.
Apply Subq_atleastp to the current goal.
We will prove ω ⊆ real.
Apply Subq_tra ω (SNoS_ ω) real to the current goal.
We will prove ω ⊆ SNoS_ ω.
An exact proof term for the current goal is omega_SNoS_omega.
We will prove SNoS_ ω ⊆ real.
An exact proof term for the current goal is SNoS_omega_real.
An exact proof term for the current goal is form100_22_real_uncountable_equip.
∎