let x be variable; :: thesis: varcl {x} = (vars x) \/ {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 Th16;
varcl {x} = (varcl A) \/ {x} by A1, Lem8;
hence varcl {x} = (vars x) \/ {x} by A1, MCART_1:7; :: thesis: verum