theorem Th3: :: NECKLA_2:3

for x being set st x in FinSETS holds
x is finite