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]
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 ;
( 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 )
;
( 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 )
;
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;
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
;
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;
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 ) )
; verum