let x be Subset of FinSETS; :: thesis: ( x is finite implies x is Element of FinSETS )
assume x is finite ; :: thesis: x is Element of FinSETS
then card x in omega by CARD_3:84;
then card x in card FinSETS by CARD_3:def 15, CLASSES4:19;
hence x is Element of FinSETS by CLASSES1:1; :: thesis: verum