theorem Th1: :: LP_SPACE:1

for a, b, c being Real st a >= 0 & a < b & c > 0 holds
a to_power c < b to_power c