:: deftheorem defines OddFibs FIB_NUM2:def 6 :
for n being Nat holds OddFibs n = Prefix (FIB,(OddNAT /\ (Seg n)));