let x be Subset of FinSETS; :: thesis: ( x is finite implies x is Set of FinSETS )
assume x is finite ; :: thesis: x is Set of FinSETS
then x is Element of FinSETS by Th15;
then x is FinSETS -set ;
hence x is Set of FinSETS by Def10; :: thesis: verum