theorem Th30: :: FIB_NUM2:30

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