theorem LC5a: :: ASYMPT_2:9

for n being Nat
for a being Real st 1 <= a holds
a to_power n <= a to_power (n + 1)