let Y be non empty set ; ERl (%I Y) = id Y
A1:
union (%I Y) = Y
by EQREL_1:def 4;
A2:
ERl (%I Y) c= id Y
id Y c= ERl (%I Y)
proof
let x1,
x2 be
object ;
RELAT_1:def 3 ( not [x1,x2] in id Y or [x1,x2] in ERl (%I Y) )
assume A6:
[x1,x2] in id Y
;
[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;
verum
end;
hence
ERl (%I Y) = id Y
by A2; verum