let e be Element of OddNAT ; :: thesis: e is odd
e in OddNAT ;
then ex n being Nat st
( e = n & n is odd ) by NUMERAL2:def 2;
hence e is odd ; :: thesis: verum