theorem :: ABSRED_0:104

for X being ARS
for x, y being Element of X st x is normform & y =01=> x holds
x is_normform_of y by Lem1;