theorem Th15: :: CLASSES5:15

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