A1:
union PA = Y
by EQREL_1:def 4;

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 ) )_{1} being Equivalence_Relation of Y st

for x1, x2 being object holds

( [x1,x2] in b_{1} iff ex A being Subset of Y st

( A in PA & x1 in A & x2 in A ) ) ; :: thesis: verum

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

hence
ex b
defpred S_{1}[ object , object ] means ex A being Subset of Y st

( A in PA & $1 in A & $2 in A );

A2: for x being object st x in Y holds

S_{1}[x,x]
_{1}[x,y] holds

S_{1}[y,x]
;

A6: for x, y, z being object st S_{1}[x,y] & S_{1}[y,z] holds

S_{1}[x,z]

A11: for x, y being object holds

( [x,y] in RA iff ( x in Y & y in Y & S_{1}[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;( A in PA & $1 in A & $2 in A );

A2: for x being object st x in Y holds

S

proof

A5:
for x, y being object st S
let x be object ; :: thesis: ( x in Y implies S_{1}[x,x] )

assume x in Y ; :: thesis: S_{1}[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;assume x in Y ; :: thesis: S

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

S

A6: for x, y, z being object st S

S

proof

consider RA being Equivalence_Relation of Y such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[y,z] implies S_{1}[x,z] )

given A being Subset of Y such that A7: A in PA and

A8: ( x in A & y in A ) ; :: thesis: ( not S_{1}[y,z] or S_{1}[x,z] )

given B being Subset of Y such that A9: B in PA and

A10: ( y in B & z in B ) ; :: thesis: S_{1}[x,z]

( A = B or A misses B ) by A7, A9, EQREL_1:def 4;

hence S_{1}[x,z]
by A7, A8, A10, XBOOLE_0:3; :: thesis: verum

end;given A being Subset of Y such that A7: A in PA and

A8: ( x in A & y in A ) ; :: thesis: ( not S

given B being Subset of Y such that A9: B in PA and

A10: ( y in B & z in B ) ; :: thesis: S

( A = B or A misses B ) by A7, A9, EQREL_1:def 4;

hence S

A11: for x, y being object holds

( [x,y] in RA iff ( x in Y & y in Y & S

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

for x1, x2 being object holds

( [x1,x2] in b

( A in PA & x1 in A & x2 in A ) ) ; :: thesis: verum