theorem Th8: :: PRE_FF:8

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