theorem :: ZFMISC_1:117

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