theorem Th21: :: HILB10_7:21

for a, b, x, y being object
for f being Function st b <> x & b <> y holds
( b in (Swap (f,x,y)) . a iff b in f . a )