let x, y be object ; :: thesis: ( {x,y} \ { the Element of {x,y}} = {} iff x = y )
set z = the Element of {x,y};

hereby :: thesis: ( x = y implies {x,y} \ { the Element of {x,y}} = {} )

assume {x,y} \ { the Element of {x,y}} = {} ; :: thesis: x = y
then {x,y} c= { the Element of {x,y}} by XBOOLE_1:37;
then ( x = the Element of {x,y} & y = the Element of {x,y} ) by ZFMISC_1:20;
hence x = y ; :: thesis: verum

end;

assume x = y ; :: thesis: {x,y} \ { the Element of {x,y}} = {}
then {x,y} = {x} by ENUMSET1:29;
then { the Element of {x,y}} = {x,y} by TARSKI:def 1;
hence {x,y} \ { the Element of {x,y}} = {} by XBOOLE_1:37; :: thesis: verum