let x, y, X be set ; :: thesis: ( 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 ) ; :: thesis: X = (X \/ {x,y}) \ {x,y}
hence X = (X \/ {x,y}) \ {x,y} by A1, Th144; :: thesis: verum