now :: thesis: ( OddNAT c= FinSETS & OddNAT is denumerable )

( OddNAT c= NAT & omega c= FinSETS ) by CLASSES4:43;
hence OddNAT c= FinSETS ; :: thesis: OddNAT is denumerable
thus OddNAT is denumerable by Th4; :: thesis: verum

end;

hence OddNAT is class of FinSETS by Th31; :: thesis: verum