theorem :: ABSRED_0:112

for X being ARS st ( for x being Element of X holds x is normform ) holds
X is WN