let a, b, c be Real; :: thesis: ( a >= 0 & a < b & c > 0 implies a to_power c < b to_power c )
( a = 0 & c > 0 implies a to_power c = 0 ) by POWER:def 2;
hence ( a >= 0 & a < b & c > 0 implies a to_power c < b to_power c ) by POWER:34, POWER:37; :: thesis: verum