A1: union PA = Y by EQREL_1:def 4;
defpred S1[ object , object ] means ex A being Subset of Y st
( A in PA & $1 in A & $2 in A );
ex RA being Equivalence_Relation of Y st
for x, y being object holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
proof
A2: for x being object st x in Y holds
S1[x,x]
proof
let x be object ; :: thesis: ( x in Y implies S1[x,x] )
assume x in Y ; :: thesis: S1[x,x]
then ex Z being set st
( x in Z & Z in PA ) by A1, TARSKI:def 4;
then consider Z being non empty set such that
A3: x in Z and
A4: Z in PA ;
reconsider A = Z as Subset of Y by A4;
take A ; :: thesis: ( A in PA & x in A & x in A )
thus ( A in PA & x in A & x in A ) by A3, A4; :: thesis: verum
end;
A5: for x, y being object st S1[x,y] holds
S1[y,x] ;
A6: for x, y, z being object st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be object ; :: thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given A being Subset of Y such that A7: A in PA and
A8: ( x in A & y in A ) ; :: thesis: ( not S1[y,z] or S1[x,z] )
given B being Subset of Y such that A9: B in PA and
A10: ( y in B & z in B ) ; :: thesis: S1[x,z]
( A = B or A misses B ) by A7, A9, EQREL_1:def 4;
hence S1[x,z] by A7, A8, A10, XBOOLE_0:3; :: thesis: verum
end;
consider RA being Equivalence_Relation of Y such that
A11: for x, y being object holds
( [x,y] in RA iff ( x in Y & y in Y & S1[x,y] ) ) from EQREL_1:sch 1(A2, A5, A6);
 take RA ; :: thesis: for x, y being object holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
thus for x, y being object holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) ) by A11; :: thesis: verum
end;
hence ex b1 being Equivalence_Relation of Y st
for x1, x2 being object holds
( [x1,x2] in b1 iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) ; :: thesis: verum