theorem :: FIB_NUM3:24

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