theorem Th27: :: HILB10_7:27

for x, y being object
for F being finite set
for E being Enumeration of F st not y in union F holds
Swap (E,x,y) is Enumeration of swap (F,x,y)