let A be finite Subset of Vars ; :: thesis: varcl A is finite Subset of Vars
A c= Rank omega by Lem7, XBOOLE_1:1;
then A in Rank omega by Lem6;
then the_rank_of A in omega by CLASSES1:74;
then the_rank_of (varcl A) in omega by Lem5;
then the_rank_of (varcl A) is finite ;
hence varcl A is finite Subset of Vars by Lem4, Th13, Th17; :: thesis: verum