let f be Real_Sequence; :: thesis: for N being Element of NAT st ( for n being Element of NAT st n >= N holds
f . n <= f . (n + 1) ) holds
for n, m being Element of NAT st N <= n & n <= m holds
f . n <= f . m
let N be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n >= N holds
f . n <= f . (n + 1) ) implies for n, m being Element of NAT st N <= n & n <= m holds
f . n <= f . m )
assume A1: for n being Element of NAT st n >= N holds
f . n <= f . (n + 1) ; :: thesis: for n, m being Element of NAT st N <= n & n <= m holds
f . n <= f . m
let n, m be Element of NAT ; :: thesis: ( N <= n & n <= m implies f . n <= f . m )
assume A2: n >= N ; :: thesis: ( not n <= m or f . n <= f . m )
defpred S₁[ Nat] means f . n <= f . $1;
A3: S₁[n] ;
A4: for m being Nat st m >= n & S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( m >= n & S₁[m] implies S₁[m + 1] )
A5: m in NAT by ORDINAL1:def 13;
assume A6: ( m >= n & f . n <= f . m ) ; :: thesis: S₁[m + 1]
then m >= N by A2, XXREAL_0:2;
then f . m <= f . (m + 1) by A1, A5;
hence S₁[m + 1] by A6, XXREAL_0:2; :: thesis: verum

end;

for m being Nat st m >= n holds
S₁[m] from NAT_1:sch 8(A3, A4);
hence ( not n <= m or f . n <= f . m ) ; :: thesis: verum