theorem :: FIB_NUM3:19

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