defpred S₁[ Nat] means Fib ($1 + 1) >= $1;
(0 + 1) + 1 = 2 ;
then A1: S₁[1] 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 that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: S₁[k + 2]

hence S₁[k + 2] by Lm1, Lm2, PRE_FF:1; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: S₁[k + 2]

then 1 <= k by NAT_1:14;
then A5: 1 + (k + 1) <= k + (k + 1) by XREAL_1:6;
A6: Fib ((k + 2) + 1) = (Fib ((k + 1) + 1)) + (Fib (k + 1)) by PRE_FF:1;
A7: k + (k + 1) <= (Fib (k + 1)) + (k + 1) by A3, XREAL_1:6;
(Fib (k + 1)) + (k + 1) <= (Fib ((k + 1) + 1)) + (Fib (k + 1)) by A4, XREAL_1:6;
then k + (k + 1) <= Fib ((k + 2) + 1) by A6, A7, XXREAL_0:2;
hence S₁[k + 2] by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A8: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from FIB_NUM:sch 1(A8, A1, A2); :: thesis: verum