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

proof

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

end;

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