theorem Th17: :: ABCMIZ_1:17

for A being finite Subset of Vars
for i being Nat holds [(varcl A),i] in Vars