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;