theorem :: CLASSES5:24

for x being Set of FinSETS holds x is finite