let x be set ; :: thesis: ( x is Element of iff ( x is finite Subset of & varcl x = x ) )
set V = { (varcl A) where A is finite Subset of : verum } ;
consider A0 being finite Subset of ;
varcl A0 in { (varcl A) where A is finite Subset of : verum } ;
then reconsider V = { (varcl A) where A is finite Subset of : verum } as non empty set ;
the carrier of (InclPoset V) = V by YELLOW_1:1;
then ( x is Element of iff x in V ) ;
then ( x is Element of iff ex A being finite Subset of st x = varcl A ) ;
hence ( x is Element of iff ( x is finite Subset of & varcl x = x ) ) by Th24; :: thesis: verum