theorem :: ABSRED_0:120

for X being ARS
for x being Element of X st X is WN & X is UN* holds
nf (nf x) = nf x