A1: omega is limit_ordinal by ORDINAL1:def 11;
let x be set ; :: thesis: ( x in FinSETS implies x is finite )
assume x in FinSETS ; :: thesis: x is finite
then consider n being Ordinal such that
A2: n in omega and
A3: x in Rank n by A1, CLASSES1:31, CLASSES2:64;
reconsider n = n as Nat by A2;
x is Element of Rank n by A3;
hence x is finite ; :: thesis: verum