theorem Th24: :: FIB_NUM2:24
for n being Nat holds Fib (n + 2) = (Fib n) + (Fib (n + 1))