let f be sequence of NAT; :: thesis: ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
reconsider f = f as Real_Sequence by FUNCT_2:7;
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) by Lm6;
hence ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) ; :: thesis: verum