theorem :: FIB_NUM4:28

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