theorem :: ABSRED_0:105

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