theorem Th31: :: HILB10_7:31

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