theorem Th24: :: FIB_NUM4:24

for n being Nat st n >= 2 holds
Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]