theorem LM001: :: BINARI_6:2

for x being Nat st x <> 0 holds
ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) )