theorem Th22: :: HEYTING1:22

for A being set
for u, v being Element of (NormForm A) holds (diff u) . v [= u