theorem Lem27: :: ABSRED_0:122

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