theorem :: NTALGO_2:4

for x being Nat st 2 <= x holds
1 < LenBSeq x