Apply Cantor_atleastp with
omega.
Apply atleastp_tra with
prim4 omega,
real,
omega leaving 2 subgoals.
The subproof is completed by applying atleastp_Power_omega_real.
Apply equip_atleastp with
real,
omega.
Apply equip_sym with
omega,
real.
The subproof is completed by applying H0.