let x, y be 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))
let O be 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 R be array of O; ( [x,y] in inversions R implies [x,y] nin inversions (Swap (R,x,y)) )
assume A1:
[x,y] in inversions R
; [x,y] nin inversions (Swap (R,x,y))
then A2:
( x in dom R & y in dom R & R /. x > R /. y )
by Th46;
A3:
not R /. x < R /. y
by A1, Th46;
( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. y = R /. x )
by A2, Th30, Th32;
hence
[x,y] nin inversions (Swap (R,x,y))
by A3, Th46; verum