:: deftheorem Def1 defines LenBSeq BINARI_6:def 1 :
for x being Nat
for b₂ being non zero Nat holds
( ( x = 0 implies ( b₂ = LenBSeq x iff b₂ = 1 ) ) & ( not x = 0 implies ( b₂ = LenBSeq x iff ex n being Nat st
( 2 to_power n <= x & x < 2 to_power (n + 1) & b₂ = n + 1 ) ) ) );