theorem ThWN1: :: ABSRED_0:111

for X being ARS holds
( X is WN iff for x being Element of X ex y being Element of X st y is_normform_of x )