theorem :: ZFMISC_1:123
for x, y being object
for A being set st x <> y holds
(A \/ {x}) \ {y} = (A \ {y}) \/ {x} by Th11, XBOOLE_1:87;