theorem Th21: :: HEYTING1:21

for A being set
for K being Element of Normal_forms_on A holds K ^ (- K) = {}