let seq be Real_Sequence; :: thesis: ( seq is increasing iff for n, m being Nat st n < m holds
seq . n < seq . m )
thus ( seq is increasing 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 increasing )

proof

assume seq is increasing ; :: thesis: for n, m being Nat st n < m holds
seq . n < seq . m
then for n being Nat holds seq . n < seq . (n + 1) ;
then for n, k being Nat holds seq . n < seq . ((n + 1) + k) by Lm2;
hence for n, m being Nat st n < m holds
seq . n < seq . m by Lm2; :: thesis: verum

end;

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