let x be set ; :: thesis: ( x in FinSETS implies x is finite )
assume A1: x in FinSETS ; :: thesis: x is finite
omega is limit_ordinal by ORDINAL1:def 12;
then consider n being Ordinal such that
A2: ( n in omega & x in Rank n ) by A1, CLASSES1:35, CLASSES2:71;
reconsider n = n as natural number by A2;
x is Element of Rank n by A2;
hence x is finite ; :: thesis: verum