theorem Th29: :: HEYTING3:29

for k being Element of NAT
for V, X being set
for a being Element of (SubstPoset (V,{k})) st X in a holds
X is finite Subset of [:V,{k}:]