theorem Th3: :: TBSP_1:3

for L being Real st 0 < L & L < 1 holds
for s being Real st 0 < s holds
ex n being Nat st L to_power n < s