theorem Th27: :: FIB_NUM2:27
for n being Nat holds Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))