let n be Nat; :: thesis: ( n > 2 implies Fib n >= 2 )
assume n > 2 ; :: thesis: Fib n >= 2
then n >= 2 + 1 by NAT_1:13;
hence Fib n >= 2 by FIB_NUM2:22, FIB_NUM2:45; :: thesis: verum