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