let A be finite Subset of Vars; :: thesis: varcl A is finite Subset of Vars
A c= Rank omega by Th23;
then A in Rank omega by Th22;
then the_rank_of A in omega by CLASSES1:66;
then the_rank_of (varcl A) is finite by Th21;
hence varcl A is finite Subset of Vars by Th9, Th19, Th20; :: thesis: verum