let Y be non empty set ; :: thesis: ERl (%I Y) = id Y
A1: union (%I Y) = Y by EQREL_1:def 4;
A2: ERl (%I Y) c= id Y

proof

let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in ERl (%I Y) or [x1,x2] in id Y )
assume [x1,x2] in ERl (%I Y) ; :: thesis: [x1,x2] in id Y
then consider a being Subset of Y such that
A3: a in %I Y and
A4: ( x1 in a & x2 in a ) by Def6;
%I Y = { {x} where x is Element of Y : verum } by EQREL_1:37;
then consider x being Element of Y such that
A5: a = {x} by A3;
( x1 = x & x2 = x ) by A4, A5, TARSKI:def 1;
hence [x1,x2] in id Y by RELAT_1:def 10; :: thesis: verum

end;

id Y c= ERl (%I Y)

proof

let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in id Y or [x1,x2] in ERl (%I Y) )
assume A6: [x1,x2] in id Y ; :: thesis: [x1,x2] in ERl (%I Y)
then A7: x1 in Y by RELAT_1:def 10;
A8: x1 = x2 by A6, RELAT_1:def 10;
ex y being set st
( x1 in y & y in %I Y ) by A1, A7, TARSKI:def 4;
hence [x1,x2] in ERl (%I Y) by A8, Def6; :: thesis: verum

end;

hence ERl (%I Y) = id Y by A2; :: thesis: verum