theorem LM000: :: BINARI_6:1

for x being Nat ex m being Nat st x < 2 to_power m