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