theorem EXL2: :: NTALGO_2:5

for n being Nat st 0 < n holds
LenBSeq n = [\(log (2,n))/] + 1