theorem Th29: :: FIB_NUM2:29
for n being Nat holds Fib (n + 1) = (Fib (n + 2)) - (Fib n)