theorem Th12: :: HILB10_7:12

for x, y being object holds swap ({},x,y) = {}