theorem :: FIB_NUM3:27

for n being Element of NAT holds (Lucas (n + 3)) * (Lucas n) = ((Lucas (n + 2)) |^ 2) - ((Lucas (n + 1)) |^ 2)