theorem :: FIB_NUM3:20

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