:: deftheorem Def300 defines EqBL2Nat BINARI_6:def 8 :
for b₁ being Equivalence_Relation of (BOOLEAN *) holds
( b₁ = EqBL2Nat iff for x, y being object holds
( [x,y] in b₁ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) );