theorem :: ZFMISC_1:121

for x, y being object
for X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}