theorem LemN1: :: ABSRED_0:101

for X being ARS
for x, y being Element of X st x is normform & x =*=> y holds
x = y