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