theorem Th103: :: NUMBER08:103

for m, n being Nat st m < n holds
(3 |^ m) - (3 to_power (1 - m)) < (3 |^ n) - (3 to_power (1 - n))