let EqR1, EqR2 be Equivalence_Relation of (BOOLEAN *); ( ( for x, y being object holds
( [x,y] in EqR1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) & ( for x, y being object holds
( [x,y] in EqR2 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) ) implies EqR1 = EqR2 )
assume that
A1:
for x, y being object holds
( [x,y] in EqR1 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) )
and
A2:
for x, y being object holds
( [x,y] in EqR2 iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) )
; EqR1 = EqR2
for a, b being object holds
( [a,b] in EqR1 iff [a,b] in EqR2 )
hence
EqR1 = EqR2
; verum