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 A0: for a, b being ordinal number 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 Z0: inversions R <> {} ; :: thesis: contradiction
then the Element of inversions R in inversions R ;
then consider a, b being Element of dom R such that
A1: ( the Element of inversions R = [a,b] & a in b & R /. a > R /. b ) ;
R <> {} by Z0;
then R /. a <= R /. b by A0, A1;
hence contradiction by A1, LemO; :: thesis: verum

end;

assume Z1: inversions R = {} ; :: thesis: R is ascending
let a be ordinal number ; :: according to EXCHSORT:def 10 :: thesis: for b being ordinal number st a in dom R & b in dom R & a in b holds
R /. a <= R /. b
let b be ordinal number ; :: 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 Z1, LemO; :: thesis: verum