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

proof

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

end;

assume A1: for n, m being Nat st n <= m holds
seq . n <= seq . m ; :: thesis: seq is non-decreasing
let n be Nat; :: according to SEQM_3:def 3 :: 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