let R be Relation; :: thesis: ( R is odd-valued implies ( R is non-zero & R is natural-valued ) )
assume A1: R is odd-valued ; :: thesis: ( R is non-zero & R is natural-valued )
OddNAT c= NAT ;
then A2: rng R c= NAT by A1;
not 0 in rng R
proof
assume 0 in rng R ; :: thesis: contradiction
then 0 is odd by A1, Th2;
hence contradiction ; :: thesis: verum
end;
hence ( R is non-zero & R is natural-valued ) by ORDINAL1:def 15, A2, VALUED_0:def 6; :: thesis: verum