theorem Th35: :: POWER:35

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