let x, y be object ; for X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}
let X be set ; ( not x in X & not y in X implies X = (X \/ {x,y}) \ {x,y} )
A1:
(X \/ {x,y}) \ {x,y} = X \ {x,y}
by XBOOLE_1:40;
assume
( not x in X & not y in X )
; X = (X \/ {x,y}) \ {x,y}
hence
X = (X \/ {x,y}) \ {x,y}
by A1, Th119; verum