theorem Th2: :: TBSP_1:2

for L being Real st 0 < L & L < 1 holds
for k being Nat holds
( L to_power k <= 1 & 0 < L to_power k )