theorem Th72: :: EXCHSORT:72

for x, y being set
for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R