now

let x be set ; :: thesis: ( x in {1} implies x in OddNAT /\ {1} )
assume A1: x in {1} ; :: thesis: x in OddNAT /\ {1}
then x = (2 * 0 ) + 1 by TARSKI:def 1;
then x in OddNAT ;
hence x in OddNAT /\ {1} by A1, XBOOLE_0:def 4; :: thesis: verum

end;

then A2: {1} c= OddNAT /\ {1} by TARSKI:def 3;
1 in NAT ;
then A3: 1 in dom FIB by FUNCT_2:def 1;
for x being set st x in OddNAT /\ {1} holds
x in {1} by XBOOLE_0:def 4;
then OddNAT /\ {1} c= {1} by TARSKI:def 3;
then OddNAT /\ {1} = {1} by A2, XBOOLE_0:def 10;
then OddFibs 1 = <*(FIB . 1)*> by A3, FINSEQ_1:4, GRFUNC_1:89, PNPROC_1:3
.= <*1*> by Def2, PRE_FF:1 ;
hence OddFibs 1 = <*1*> ; :: thesis: verum