let x, y be set ; :: thesis: for O being non empty connected Poset
for R being array of O holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let O be non empty connected Poset; :: thesis: for R being array of O holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let R be array of O; :: thesis: ( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )

hereby :: thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R )

assume A1: [x,y] in inversions R ; :: thesis: ( x in dom R & y in dom R & x in y & R /. x > R /. y )
then reconsider R1 = R as non empty Function ;
consider a, b being Element of dom R1 such that
A0: ( [x,y] = [a,b] & a in b & not R /. a <= R /. b ) by A1;
( x = a & y = b ) by A0, ZFMISC_1:27;
hence ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by A0, LemO; :: thesis: verum

end;

thus ( x in dom R & y in dom R & x in y & R /. x > R /. y implies [x,y] in inversions R ) ; :: thesis: verum