let x, y, z be set ; :: thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds
[z,y] in inversions R
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) holds
[z,y] in inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R & x in z & [z,y] in inversions (Swap (R,x,y)) implies [z,y] in inversions R )
assume [x,y] in inversions R ; :: thesis: ( not x in z or not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R )
then A0: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by TW0;
A1: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
assume Z2: x in z ; :: thesis: ( not [z,y] in inversions (Swap (R,x,y)) or [z,y] in inversions R )
assume [z,y] in inversions (Swap (R,x,y)) ; :: thesis: [z,y] in inversions R
then A2: ( z in dom R & z in y & (Swap (R,x,y)) /. z > (Swap (R,x,y)) /. y ) by A1, TW0;
then ( z <> x & z <> y ) by Z2;
then ( (Swap (R,x,y)) /. y = R /. x & (Swap (R,x,y)) /. z = R /. z ) by A0, A2, TSb2, TSc2;
then R /. z > R /. y by A0, A2, ORDERS_2:5;
hence [z,y] in inversions R by A0, A2; :: thesis: verum