:: deftheorem Def110 defines BL2Nat BINARI_6:def 7 :
for b₁ being Function of (BOOLEAN *),NAT holds
( b₁ = BL2Nat iff for x being Element of BOOLEAN * holds b₁ . x = ExAbsval x );