theorem :: NTALGO_2:7

Nat2BL . 1 = <*1*>