hereby :: thesis: ( ( for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. m < s /. n ) implies s is descending )

assume A2:
for n, m being Nat st n in dom s & m in dom s & n < m holds s /. m < s /. n ) implies s is descending )

assume A1:
s is descending
; :: thesis: for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. m < s /. n

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. m < s /. n )

assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. m < s /. n

then s /. m <~ s /. n by A1;

hence s /. m < s /. n by ORDERS_2:def 6; :: thesis: verum

end;s /. m < s /. n

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. m < s /. n )

assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. m < s /. n

then s /. m <~ s /. n by A1;

hence s /. m < s /. n by ORDERS_2:def 6; :: thesis: verum

s /. m < s /. n ; :: thesis: s is descending

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

s /. m <~ s /. n

hence
s is descending
; :: thesis: verums /. m <~ s /. n

let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. m <~ s /. n )

assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. m <~ s /. n

then s /. m < s /. n by A2;

then ( s /. m <= s /. n & s /. m <> s /. n ) by ORDERS_2:def 6;

hence s /. m <~ s /. n by ORDERS_2:2; :: thesis: verum

end;assume ( n in dom s & m in dom s & n < m ) ; :: thesis: s /. m <~ s /. n

then s /. m < s /. n by A2;

then ( s /. m <= s /. n & s /. m <> s /. n ) by ORDERS_2:def 6;

hence s /. m <~ s /. n by ORDERS_2:2; :: thesis: verum