Assume H1: equip real ω.

Apply form100_22_real_uncountable_atleastp to the current goal.

We will prove atleastp real ω.

Apply equip_atleastp real ω to the current goal.

An exact proof term for the current goal is H1.

∎