let f be Real_Sequence; :: thesis: for N being Nat st ( for n being Nat st n >= N holds
f . n <= f . (n + 1) ) holds
for n, m being Nat st N <= n & n <= m holds
f . n <= f . m
let N be Nat; :: thesis: ( ( for n being Nat st n >= N holds
f . n <= f . (n + 1) ) implies for n, m being Nat st N <= n & n <= m holds
f . n <= f . m )
assume A1: for n being Nat st n >= N holds
f . n <= f . (n + 1) ; :: thesis: for n, m being Nat st N <= n & n <= m holds
f . n <= f . m
let n, m be Nat; :: thesis: ( N <= n & n <= m implies f . n <= f . m )
defpred S₁[ Nat] means f . n <= f . $1;
assume A2: n >= N ; :: thesis: ( not n <= m or f . n <= f . m )
A3: 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] )
assume that
A4: m >= n and
A5: f . n <= f . m ; :: thesis: S₁[m + 1]
( m in NAT & m >= N ) by A2, A4, ORDINAL1:def 12, XXREAL_0:2;
then f . m <= f . (m + 1) by A1;
hence S₁[m + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

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