theorem Th31: :: CLASSES5:31

for X being non finite Subset of FinSETS holds X is class of FinSETS