theorem Lem22: :: ABSRED_0:117

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