let x be Set of FinSETS ; :: thesis: x is finite
x is FinSETS -set by Def10;
then card x in card FinSETS by CLASSES4:30;
then card x in omega by CLASSES4:19, CARD_3:def 15;
hence x is finite ; :: thesis: verum