theorem Th18: :: ABCMIZ_1:18

Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }