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 & y in z & [x,z] in inversions (Swap (R,x,y)) holds
[y,z] in inversions R
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) holds
[y,z] in inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R & y in z & [x,z] in inversions (Swap (R,x,y)) implies [y,z] in inversions R )
assume [x,y] in inversions R ; :: thesis: ( not y in z or not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R )
then A1: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
A2: dom (Swap (R,x,y)) = dom R by FUNCT_7:99;
assume A3: y in z ; :: thesis: ( not [x,z] in inversions (Swap (R,x,y)) or [y,z] in inversions R )
assume [x,z] in inversions (Swap (R,x,y)) ; :: thesis: [y,z] in inversions R
then A4: ( z in dom R & x in z & (Swap (R,x,y)) /. x > (Swap (R,x,y)) /. z ) by A2, Th46;
then ( z <> x & z <> y ) by A3;
then ( (Swap (R,x,y)) /. x = R /. y & (Swap (R,x,y)) /. z = R /. z ) by A1, A4, Th30, Th34;
hence [y,z] in inversions R by A1, A4, A3; :: thesis: verum