let R be Relation; :: thesis: ( R is empty implies R is odd-valued )
assume R is empty ; :: thesis: R is odd-valued
then rng R c= OddNAT ;
hence R is odd-valued ; :: thesis: verum