Proofgold Proof

pf
Apply andI with atleastp omega real, not (equip real omega) leaving 2 subgoals. Apply Subq_atleastp with omega, real. Apply Subq_tra with omega, SNoS_ omega, real leaving 2 subgoals. The subproof is completed by applying omega_SNoS_omega. The subproof is completed by applying SNoS_omega_real. The subproof is completed by applying form100_22_real_uncountable_equip. ■