theorem Th28: :: FIB_NUM2:28
for n being Nat holds Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1))