let O be non empty connected Poset; :: thesis: for R being array of O
for x being object
for y being set 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: for x being object
for y being set holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let x be object ; :: thesis: for y being set holds
( [x,y] in inversions R iff ( x in dom R & y in dom R & x in y & R /. x > R /. y ) )
let y be set ; :: 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
A2: ( [x,y] = [a,b] & a in b & not R /. a <= R /. b ) by A1;
( x = a & y = b ) by A2, XTUPLE_0:1;
hence ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by A2, Th45; :: 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