theorem LM0710: :: BINARI_6:25

for x being Element of BOOLEAN * st x in rng Nat2BL holds
1 <= len x