theorem Lem23: :: ABSRED_0:118

for X being ARS
for x, y being Element of X st X is WN & X is UN* & y is_normform_of x holds
y = nf x