let O be non empty connected Poset; :: thesis: for R being array of O holds
( R is ascending iff inversions R = {} )
let R be array of O; :: thesis: ( R is ascending iff inversions R = {} )
thus ( R is ascending implies inversions R = {} ) :: thesis: ( inversions R = {} implies R is ascending )

proof

assume A1: for a, b being Ordinal st a in dom R & b in dom R & a in b holds
R /. a <= R /. b ; :: according to EXCHSORT:def 10 :: thesis: inversions R = {}
set x = the Element of inversions R;
assume A2: inversions R <> {} ; :: thesis: contradiction
then the Element of inversions R in inversions R ;
then consider a, b being Element of dom R such that
A3: ( the Element of inversions R = [a,b] & a in b & R /. a > R /. b ) ;
R <> {} by A2;
then R /. a <= R /. b by A1, A3;
hence contradiction by A3, Th45; :: thesis: verum

end;

assume A4: inversions R = {} ; :: thesis: R is ascending
let a be Ordinal; :: according to EXCHSORT:def 10 :: thesis: for b being Ordinal st a in dom R & b in dom R & a in b holds
R /. a <= R /. b
let b be Ordinal; :: thesis: ( a in dom R & b in dom R & a in b implies R /. a <= R /. b )
assume ( a in dom R & b in dom R & a in b ) ; :: thesis: R /. a <= R /. b
then ( R /. a > R /. b implies [a,b] in inversions R ) ;
hence R /. a <= R /. b by A4, Th45; :: thesis: verum