let x be variable; :: thesis: varcl (vars x) = vars x
x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A1: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
vars x = varcl A by A1;
hence varcl (vars x) = vars x ; :: thesis: verum