theorem Lem24: :: ABSRED_0:119

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