theorem LemN2: :: ABSRED_0:102

for X being ARS
for x being Element of X st x is normform holds
x is_normform_of x ;