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 A2:
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;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

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

hence
s is ascending
; :: thesis: verums /. 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;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