theorem Th3: :: LPSPACE2:3

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