hereby :: thesis: ( ( for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n < s /. m ) implies s is ascending )

assume A1: s is ascending ; :: thesis: for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n < s /. m
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. n < s /. m )
assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. n < s /. m
then s /. n <~ s /. m by A1;
hence s /. n < s /. m by ORDERS_2:def 6; :: thesis: verum

end;

assume A2: for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n < s /. m ; :: thesis: s is ascending

now :: thesis: for n, m being Nat st n in dom s & m in dom s & n < m holds
s /. n <~ s /. m

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. n <~ s /. m )
assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. n <~ s /. m
then s /. n < s /. m by A2;
then ( s /. n <= s /. m & s /. n <> s /. m ) by ORDERS_2:def 6;
hence s /. n <~ s /. m by ORDERS_2:2; :: thesis: verum

end;

hence s is ascending ; :: thesis: verum