:: deftheorem defines swap HILB10_7:def 3 :
for X being set
for a, b being object holds swap (X,a,b) = { ((A \ {a}) \/ {b}) where A is Element of X : a in A } \/ { (A \/ {a}) where A is Element of X : ( not a in A & A in X ) } ;