defpred S₁[ object , object ] means BL2Nat . $1 = BL2Nat . $2;
A1: for x being object st x in BOOLEAN * holds
S₁[x,x] ;
A2: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] ;
consider EqR being Equivalence_Relation of (BOOLEAN *) such that
A4: for x, y being object holds
( [x,y] in EqR iff ( x in BOOLEAN * & y in BOOLEAN * & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A2, A3);
thus ex b₁ being Equivalence_Relation of (BOOLEAN *) st
for x, y being object holds
( [x,y] in b₁ iff ( x in BOOLEAN * & y in BOOLEAN * & BL2Nat . x = BL2Nat . y ) ) by A4; :: thesis: verum