theorem :: GRAPH_2:63

for f being FinSequence of INT
for m, n being Nat st m >= n holds
f is_non_decreasing_on m,n