theorem Th2: :: EULRPART:2

for n being Nat holds
( n in OddNAT iff n is odd )