theorem Th9: :: HEYTING2:9

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