let seq be Real_Sequence; :: thesis: ( seq is increasing iff for n, m being Element of NAT st n < m holds
seq . n < seq . m )
thus ( seq is increasing implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) :: thesis: ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies seq is increasing )

proof

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

end;

assume A1: for n, m being Element of NAT st n < m holds
seq . n < seq . m ; :: thesis: seq is increasing
let n be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for n being Element of NAT st n in dom seq & n in dom seq & n < n holds
seq . n < seq . n
let m be Element of NAT ; :: thesis: ( n in dom seq & m in dom seq & n < m implies seq . n < seq . m )
assume ( n in dom seq & m in dom seq & n < m ) ; :: thesis: seq . n < seq . m
hence seq . n < seq . m by A1; :: thesis: verum