theorem :: FIB_NUM3:22

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