let x, y, X be set ; :: thesis: ( not x in X & not y in X implies X = (X \/ {x,y}) \ {x,y} )
assume ( not x in X & not y in X ) ; :: thesis: X = (X \/ {x,y}) \ {x,y}
then ( (X \/ {x,y}) \ {x,y} = X \ {x,y} & X \ {x,y} = X ) by Th144, XBOOLE_1:40;
hence X = (X \/ {x,y}) \ {x,y} ; :: thesis: verum