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] and
A is finite by Th18;
varcl {x} = (varcl A) \/ {x} by A1, Th26;
hence varcl {x} = (vars x) \/ {x} by A1; :: thesis: verum