theorem Th25: :: FIB_NUM2:25

for n being Nat holds Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))