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
[y,x] nin inversions R
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R holds
[y,x] nin inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R implies [y,x] nin inversions R )
assume [x,y] in inversions R ; :: thesis: [y,x] nin inversions R
then y nin x by TW0;
hence [y,x] nin inversions R by TW0; :: thesis: verum