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

proof

assume seq is non-decreasing ; :: thesis: for n, k being Element of NAT holds seq . n <= seq . (n + k)
then for n being Element of NAT holds seq . n <= seq . (n + 1) by Lm8;
hence for n, k being Element of NAT holds seq . n <= seq . (n + k) by Lm4; :: thesis: verum

end;

assume for n, k being Element of NAT holds seq . n <= seq . (n + k) ; :: thesis: seq is non-decreasing
then for n being Element of NAT holds seq . n <= seq . (n + 1) ;
hence seq is non-decreasing by Lm8; :: thesis: verum