:: deftheorem defines Lucas FIB_NUM3:def 2 :
for n being Nat holds Lucas n = (Lucas . n) `1 ;