theorem LM031: :: BINARI_6:11

rng Nat2BL = { x where x is Element of BOOLEAN * : x . (len x) = 1 } \/ {<*0*>}