let n be Nat; :: thesis: ( n in OddNAT iff n is odd )
thus ( n in OddNAT implies n is odd ) :: thesis: ( n is odd implies n in OddNAT )

proof

assume n in OddNAT ; :: thesis: n is odd
then ex i being Element of NAT st n = (2 * i) + 1 by FIB_NUM2:def 4;
hence n is odd ; :: thesis: verum

end;

assume n is odd ; :: thesis: n in OddNAT
then consider i being Nat such that
A1: n = (2 * i) + 1 by ABIAN:9;
i in NAT by ORDINAL1:def 12;
hence n in OddNAT by A1, FIB_NUM2:def 4; :: thesis: verum