let x be Nat; :: thesis: ( 2 <= x implies 1 < LenBSeq x )

assume AS0: 2 <= x ; :: thesis: 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; :: thesis: verum

assume AS0: 2 <= x ; :: thesis: 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; :: thesis: verum