theorem Th13: :: HILB10_7:13

for x, y being object
for X, Y being set holds swap ((X \/ Y),x,y) = (swap (X,x,y)) \/ (swap (Y,x,y))