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

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

end;

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