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

A1: union (%I Y) = Y by EQREL_1:def 4;

A2: ERl (%I Y) c= id Y

proof

id Y c= ERl (%I Y)
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;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

proof

hence
ERl (%I Y) = id Y
by A2; :: thesis: verum
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;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