theorem Th73: :: EXCHSORT:73

for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)