:: deftheorem Def1 defines odd-valued EULRPART:def 1 :
for R being Relation holds
( R is odd-valued iff rng R c= OddNAT );