theorem Th36: :: POWER:36

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