theorem Th39: :: POWER:39
for a, b, c being Real st a < b & c > 1 holds
c to_power a < c to_power b