theorem Th31: :: FIB_NUM2:31

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