theorem Th3: :: HOLDER_1:3

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