theorem Th1: :: TBSP_1:1

for L being Real st 0 < L & L < 1 holds
for n, m being Nat st n <= m holds
L to_power m <= L to_power n