defpred S1[ 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: S1[3] by Th22, Th23;
A3: for k being non trivial Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be non trivial Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A4: S1[k] ; :: thesis: ( not S1[k + 1] or S1[k + 2] )
assume S1[k + 1] ; :: thesis: S1[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 S1[k + 2] ; :: thesis: verum
end;
A5: S1[2] by Th21, Th22;
for n being non trivial Nat holds S1[n] from FIB_NUM2:sch 2(A5, A2, A3);
 hence Fib n < Fib (n + 1) by A1; :: thesis: verum