theorem LM007: :: BINARI_6:7

for x being Nat holds x = Absval ((LenBSeq x) -BinarySequence x)