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 CARD_3:def 15, CLASSES4:19;
hence x is finite ; :: thesis: verum