let Y be set ; :: thesis: for X being Subset of (EqRelLatt Y)
for R being Relation st R = union X holds
R = R ~
let X be Subset of (EqRelLatt Y); :: thesis: for R being Relation st R = union X holds
R = R ~
let R be Relation; :: thesis: ( R = union X implies R = R ~ )
assume A1: R = union X ; :: thesis: R = R ~

now :: thesis: for x, y being object holds
( ( [x,y] in R implies [x,y] in R ~ ) & ( [x,y] in R ~ implies [x,y] in R ) )

let x, y be object ; :: thesis: ( ( [x,y] in R implies [x,y] in R ~ ) & ( [x,y] in R ~ implies [x,y] in R ) )
thus ( [x,y] in R implies [x,y] in R ~ ) :: thesis: ( [x,y] in R ~ implies [x,y] in R )

proof

assume [x,y] in R ; :: thesis: [x,y] in R ~
then consider Z being set such that
A2: [x,y] in Z and
A3: Z in X by A1, TARSKI:def 4;
reconsider Z = Z as Equivalence_Relation of Y by A3, MSUALG_5:21;
[y,x] in Z by A2, EQREL_1:6;
then [y,x] in R by A1, A3, TARSKI:def 4;
hence [x,y] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

thus ( [x,y] in R ~ implies [x,y] in R ) :: thesis: verum

proof

assume [x,y] in R ~ ; :: thesis: [x,y] in R
then [y,x] in R by RELAT_1:def 7;
then consider Z being set such that
A4: [y,x] in Z and
A5: Z in X by A1, TARSKI:def 4;
reconsider Z = Z as Equivalence_Relation of Y by A5, MSUALG_5:21;
[x,y] in Z by A4, EQREL_1:6;
hence [x,y] in R by A1, A5, TARSKI:def 4; :: thesis: verum

end;

end;

hence R = R ~ by RELAT_1:def 2; :: thesis: verum