theorem Th3: :: HEYTING1:3

for A being set
for K being Element of Normal_forms_on A holds mi (K ^ K) = K