:: deftheorem defines Fibonacci NUMBER06:def 6 :
for n being Nat holds
( n is Fibonacci iff ex k being Nat st n = Fib k );