let X be non finite Subset of FinSETS; :: thesis: X is class of FinSETS
X is FinSETS -Class ;
hence X is class of FinSETS by Def12; :: thesis: verum