theorem Th12: :: FIB_NUM3:12

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