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

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