theorem :: CLASSES5:16

for X being finite set st X c= FinSETS holds
X in FinSETS