theorem Th51: :: EXCHSORT:51

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
[x,y] nin inversions (Swap (R,x,y))