theorem Th11: :: FIB_NUM3:11

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