let n be Element of NAT ; :: thesis: ( n > 1 implies Fib n < Fib (n + 1) )
assume A1: n > 1 ; :: thesis: Fib n < Fib (n + 1)
A2: not n is trivial by A1, NAT_2:def 1;
defpred S₁[ Nat] means Fib $1 < Fib ($1 + 1);
A3: S₁[2] by Th23, Th24;
A4: S₁[3] by Th24, Th25;
A5: 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 A6: 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 A6, XREAL_1:10;
then Fib (k + 2) < (Fib (k + 1)) + (Fib (k + 2)) by Th26;
then Fib (k + 2) < Fib (k + 3) by Th27;
hence S₁[k + 2] ; :: thesis: verum

end;

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