let f be FinSequence of INT ; :: thesis: for m, n being Element of NAT st m >= n holds
f is_non_decreasing_on m,n
let m, n be Element of NAT ; :: thesis: ( m >= n implies f is_non_decreasing_on m,n )
assume A1: m >= n ; :: thesis: f is_non_decreasing_on m,n

per cases ( m = n or m > n ) by A1, XXREAL_0:1;

suppose m = n ; :: thesis: f is_non_decreasing_on m,n

hence f is_non_decreasing_on m,n by Lm1; :: thesis: verum

end;

suppose A2: m > n ; :: thesis: f is_non_decreasing_on m,n

now

let i, j be Element of NAT ; :: thesis: ( m <= i & i <= j & j <= n implies not f . i > f . j )
assume that
A3: ( m <= i & i <= j ) and
A4: j <= n ; :: thesis: not f . i > f . j
assume f . i > f . j ; :: thesis: contradiction
m <= j by A3, XXREAL_0:2;
hence contradiction by A2, A4, XXREAL_0:2; :: thesis: verum

end;

hence f is_non_decreasing_on m,n by GRAPH_2:def 13; :: thesis: verum

end;

end;