set A = EqRel (R,I);
consider B being Equivalence_Relation of the carrier of R such that
A1:
for x, y being object holds
( [x,y] in B iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st
( P = x & Q = y & P - Q in I ) ) )
by Lm1;
EqRel (R,I) = B
proof
let x,
y be
object ;
RELAT_1:def 2 ( ( not [x,y] in EqRel (R,I) or [x,y] in B ) & ( not [x,y] in B or [x,y] in EqRel (R,I) ) )
thus
(
[x,y] in EqRel (
R,
I) implies
[x,y] in B )
( not [x,y] in B or [x,y] in EqRel (R,I) )
assume
[x,y] in B
;
[x,y] in EqRel (R,I)
then
ex
P,
Q being
Element of
R st
(
P = x &
Q = y &
P - Q in I )
by A1;
hence
[x,y] in EqRel (
R,
I)
by Def5;
verum
end;
hence
( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive )
by EQREL_1:9, RELAT_1:40; verum