defpred S₁[ Nat] means Fib $1 < Fib ($1 + 1);
let n be Nat; :: thesis: ( n > 1 implies Fib n < Fib (n + 1) )
assume n > 1 ; :: thesis: Fib n < Fib (n + 1)
then A1: not n is trivial by NAT_2:def 1;
A2: S₁[3] by Th22, Th23;
A3: for k being non trivial Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be non trivial Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume A4: 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 A4, XREAL_1:8;
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;

A5: S₁[2] by Th21, Th22;
for n being non trivial Nat holds S₁[n] from FIB_NUM2:sch 2(A5, A2, A3);
hence Fib n < Fib (n + 1) by A1; :: thesis: verum