theorem Th12: :: HEYTING2:12

for V being set
for C being finite set
for A being Element of SubstitutionSet (V,C) holds mi (A ^ (- A)) = Bottom (SubstLatt (V,C))