now :: thesis: for m being Nat ex n being Nat st
( n >= m & n in OddNAT )

let m be Nat; :: thesis: ex n being Nat st
( n >= m & n in OddNAT )
reconsider n = (2 * m) + 1 as Element of NAT by ORDINAL1:def 12;

now :: thesis: ( n >= m & n in OddNAT )

1 * m <= 2 * m by NAT_1:4;
hence n >= m by NAT_1:12; :: thesis: n in OddNAT
m is Element of NAT by ORDINAL1:def 12;
hence n in OddNAT by FIB_NUM2:def 4; :: thesis: verum

end;

hence ex n being Nat st
( n >= m & n in OddNAT ) ; :: thesis: verum

end;

then OddNAT is infinite by PYTHTRIP:9;
hence OddNAT is denumerable ; :: thesis: verum