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