let x be Nat; ( 2 <= x implies 1 < LenBSeq x )
assume AS0:
2 <= x
; 1 < LenBSeq x
then consider n being Nat such that
P3:
( 2 to_power n <= x & x < 2 to_power (n + 1) & LenBSeq x = n + 1 )
by BINARI_6:def 1;
n <> 0
by AS0, P3;
then
0 + 1 < n + 1
by XREAL_1:8;
hence
1 < LenBSeq x
by P3; verum