let a, b, c be Real; :: thesis: ( a <= b & c >= 1 implies c to_power a <= c to_power b )
assume a <= b ; :: thesis: ( not c >= 1 or c to_power a <= c to_power b )
then A1: ( a < b or a = b ) by XXREAL_0:1;
assume c >= 1 ; :: thesis: c to_power a <= c to_power b

per cases then ( c > 1 or c = 1 ) by XXREAL_0:1;

suppose c > 1 ; :: thesis: c to_power a <= c to_power b

hence c to_power a <= c to_power b by A1, POWER:39; :: thesis: verum

end;

suppose A2: c = 1 ; :: thesis: c to_power a <= c to_power b

( 1 to_power a = 1 & 1 to_power b = 1 ) by POWER:26;
hence c to_power a <= c to_power b by A2; :: thesis: verum

end;

end;