let Y be non empty set ; ERl (%I Y) = id Y
A1:
union (%I Y) = Y
by EQREL_1:def 6;
A2:
ERl (%I Y) c= id Y
proof
let x1,
x2 be
set ;
RELAT_1:def 3 ( not [x1,x2] in ERl (%I Y) or [x1,x2] in id Y )
assume A3:
[x1,x2] in ERl (%I Y)
;
[x1,x2] in id Y
consider a being
Subset of
Y such that A4:
a in %I Y
and A5:
(
x1 in a &
x2 in a )
by A3, Def6;
A6:
%I Y = { {x} where x is Element of Y : verum }
by EQREL_1:46;
consider x being
Element of
Y such that A7:
a = {x}
by A4, A6;
A8:
(
x1 = x &
x2 = x )
by A5, A7, TARSKI:def 1;
thus
[x1,x2] in id Y
by A8, RELAT_1:def 10;
verum
end;
A9:
id Y c= ERl (%I Y)
proof
let x1,
x2 be
set ;
RELAT_1:def 3 ( not [x1,x2] in id Y or [x1,x2] in ERl (%I Y) )
assume A10:
[x1,x2] in id Y
;
[x1,x2] in ERl (%I Y)
A11:
x1 in Y
by A10, RELAT_1:def 10;
A12:
x1 = x2
by A10, RELAT_1:def 10;
A13:
ex
y being
set st
(
x1 in y &
y in %I Y )
by A1, A11, TARSKI:def 4;
thus
[x1,x2] in ERl (%I Y)
by A12, A13, Def6;
verum
end;
thus
ERl (%I Y) = id Y
by A2, A9, XBOOLE_0:def 10; verum