let x be Element of BOOLEAN * ; :: thesis: ( x in rng Nat2BL implies 1 <= len x )
assume x in rng Nat2BL ; :: thesis: 1 <= len x
then consider L being Element of NAT such that
H5: x = Nat2BL . L by FUNCT_2:113;
x = (LenBSeq L) -BinarySequence L by Def2, H5;
then 0 <> len x ;
then 0 < len x ;
then 1 + 0 <= len x by NAT_1:13;
hence 1 <= len x ; :: thesis: verum