let seq be Real_Sequence; :: thesis: ( seq is non-increasing iff for n, m being Nat st n <= m holds
seq . m <= seq . n )
thus ( seq is non-increasing implies for n, m being Nat st n <= m holds
seq . m <= seq . n ) :: thesis: ( ( for n, m being Nat st n <= m holds
seq . m <= seq . n ) implies seq is non-increasing )

proof

assume seq is non-increasing ; :: thesis: for n, m being Nat st n <= m holds
seq . m <= seq . n
then for n, k being Nat holds seq . (n + k) <= seq . n by Th7;
hence for n, m being Nat st n <= m holds
seq . m <= seq . n by Lm5; :: thesis: verum

end;

assume A1: for n, m being Nat st n <= m holds
seq . m <= seq . n ; :: thesis: seq is non-increasing
let n be Nat; :: according to SEQM_3:def 4 :: thesis: for n being Nat st n in dom seq & n in dom seq & n <= n holds
seq . n >= seq . n
let m be Nat; :: thesis: ( n in dom seq & m in dom seq & n <= m implies seq . n >= seq . m )
assume that
n in dom seq and
m in dom seq and
A2: n <= m ; :: thesis: seq . n >= seq . m
thus seq . n >= seq . m by A1, A2; :: thesis: verum