now :: thesis: for x being object st x in {1} holds
x in OddNAT /\ {1}

let x be object ; :: 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} ;
1 in NAT ;
then A3: 1 in dom FIB by FUNCT_2:def 1;
for x being object st x in OddNAT /\ {1} holds
x in {1} by XBOOLE_0:def 4;
then OddNAT /\ {1} c= {1} ;
then OddNAT /\ {1} = {1} by A2;
then OddFibs 1 = <*(FIB . 1)*> by A3, FINSEQ_1:2, FINSEQ_3:157, GRFUNC_1:28
.= <*1*> by Def2, PRE_FF:1 ;
hence OddFibs 1 = <*1*> ; :: thesis: verum