let x, y be set ; :: thesis: 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))
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R holds
[x,y] nin inversions (Swap (R,x,y))
let R be array of O; :: thesis: ( [x,y] in inversions R implies [x,y] nin inversions (Swap (R,x,y)) )
assume Z0: [x,y] in inversions R ; :: thesis: [x,y] nin inversions (Swap (R,x,y))
then A0: ( x in dom R & y in dom R & R /. x > R /. y ) by TW0;
A1: not R /. x < R /. y by Z0, TW0;
( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x ) by A0, TSa2, TSb2;
hence [x,y] nin inversions (Swap (R,x,y)) by A1, TW0; :: thesis: verum