theorem Th13: :: FIB_NUM3:13

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