theorem Lem21: :: ABSRED_0:116

for X being ARS
for x, y, z being Element of X st y is_normform_of x & z is_normform_of x & y <> z holds
x =+=> y