let n be Nat; :: thesis: Fib n <= Fib (n + 1)
defpred S₁[ Nat] means Fib $1 <= Fib ($1 + 1);
A1: S₁[ 0 ] by PRE_FF:1;
A2: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume A3: S₁[k] ; :: thesis: ( not S₁[k + 1] or S₁[k + 2] )
assume S₁[k + 1] ; :: thesis: S₁[k + 2]
then (Fib k) + (Fib (k + 1)) <= (Fib (k + 1)) + (Fib (k + 2)) by A3, XREAL_1:7;
then Fib (k + 2) <= (Fib (k + 1)) + (Fib (k + 2)) by Th24;
then Fib (k + 2) <= Fib (k + 3) by Th25;
hence S₁[k + 2] ; :: thesis: verum

end;

A4: S₁[1] by Th21, PRE_FF:1;
for n being Nat holds S₁[n] from FIB_NUM:sch 1(A1, A4, A2);
hence Fib n <= Fib (n + 1) ; :: thesis: verum