let X be complex-membered set ; :: thesis: addRel (X,0) = id X

now :: thesis: for x, y being object holds
( ( [x,y] in addRel (X,0) implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in addRel (X,0) ) )

let x, y be object ; :: thesis: ( ( [x,y] in addRel (X,0) implies ( x in X & x = y ) ) & ( x in X & x = y implies [x,y] in addRel (X,0) ) )

hereby :: thesis: ( x in X & x = y implies [x,y] in addRel (X,0) )

assume A1: [x,y] in addRel (X,0) ; :: thesis: ( x in X & x = y )
reconsider z1 = x, z2 = y as set by TARSKI:1;
[z1,z2] in addRel (X,0) by A1;
then ( z1 in X & z2 in X ) by MMLQUER2:4;
then reconsider z1 = z1, z2 = z2 as Complex ;
[z1,z2] in addRel (X,0) by A1;
then ( z1 in X & z2 = 0 + z1 ) by Th11;
hence ( x in X & x = y ) ; :: thesis: verum

end;

assume A2: ( x in X & x = y ) ; :: thesis: [x,y] in addRel (X,0)
then reconsider z1 = x, z2 = y as Complex ;
z2 = 0 + z1 by A2;
hence [x,y] in addRel (X,0) by A2, Th11; :: thesis: verum

end;

hence addRel (X,0) = id X by RELAT_1:def 10; :: thesis: verum