:: deftheorem defines EvenFibs FIB_NUM2:def 5 :
for n being Nat holds EvenFibs n = Prefix (FIB,(EvenNAT /\ (Seg n)));