theorem :: FIB_NUM3:44

for n being Element of NAT holds (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))