theorem :: NOMIN_9:7

for n being Nat holds Lucas (0,1,1,(- 1),n) = Fib n by Th6;