theorem Th2: :: BINARI_4:2

for m being Nat holds 2 to_power m >= m