theorem :: ABSRED_0:106

for X being ARS
for x, y being Element of X st x is_normform_of y & y is_normform_of x holds
x = y by LemN1;