theorem Th10: :: HEYTING2:10

for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) st A = {} holds
- A = {{}}