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