let x, y be object ; :: thesis: for X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}
let 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, Th119; :: thesis: verum