theorem :: CLASSES5:32

NAT is class of FinSETS by Th31, CLASSES4:43;