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 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;
assume A2: for n, m being Nat st n in dom s & m in dom s & n < m holds
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
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;
hence s is descending ; :: thesis: verum