theorem :: FIB_NUM3:25

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