theorem LM006: :: BINARI_6:6

for x being Nat holds x < 2 to_power (LenBSeq x)