let a, b be non negative Real; :: thesis: for c being positive Real holds
( a >= b iff a to_power c >= b to_power c )
let c be positive Real; :: thesis: ( a >= b iff a to_power c >= b to_power c )
( b = 0 implies b to_power c = 0 ) by POWER:def 2;
then A1: ( a > b implies a to_power c >= b to_power c ) by POWER:37;
( a = 0 implies a to_power c = 0 ) by POWER:def 2;
hence ( a >= b iff a to_power c >= b to_power c ) by A1, XXREAL_0:1, POWER:37; :: thesis: verum