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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
n + 2 > 1 + 0 by XREAL_1:8;
then ( Fib ((n + 2) + 1) >= (Fib (n + 2)) + 1 & (Fib (n + 2)) + 1 >= n + 1 ) by A3, FIB_NUM2:44, NAT_1:13, XREAL_1:7;
hence S₁[n + 1] by XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence Fib (n + 2) >= n ; :: thesis: verum