:: deftheorem defines incl EXCHSORT:def 13 :
for O being non empty connected Poset
for R being array of O
for x, y being set holds (R,x,y) incl = [:(Swap ((id (dom R)),x,y)),(Swap ((id (dom R)),x,y)):] +* (id ([:{x},((succ y) \ x):] \/ [:((succ y) \ x),{y}:]));