theorem Th26: :: ABCMIZ_1:26

for j being Element of NAT
for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}