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,z] in inversions R holds
[x,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,z] in inversions R holds
[x,z] in inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R & [y,z] in inversions R implies [x,z] in inversions R )
assume Z0: ( [x,y] in inversions R & [y,z] in inversions R ) ; :: thesis: [x,z] in inversions R
then reconsider x = x, y = y, z = z as Element of dom R by TW0;
( x in y & R /. x > R /. y & y in z & R /. y > R /. z ) by Z0, TW0;
then ( x in z & R /. x > R /. z ) by ORDERS_2:5, ORDINAL1:10;
hence [x,z] in inversions R ; :: thesis: verum