theorem :: CLASSES5:25

for x being Subset of FinSETS st x is finite holds
x is Set of FinSETS