:: deftheorem Def400 defines QuBL2Nat BINARI_6:def 9 :
for b₁ being Function of (Class EqBL2Nat),NAT holds
( b₁ = QuBL2Nat iff for A being Element of Class EqBL2Nat ex x being object st
( x in A & b₁ . A = BL2Nat . x ) );