x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A1: x = [(varcl A),j] and
A2: A is finite by Th18;
x `1 = varcl A by A1;
hence for b<sub>1</sub> being set st b<sub>1</sub> = x `1 holds
b₁ is finite by A2, Th24; :: thesis: verum