let X be ARS ; :: thesis: ( ( for x being Element of X holds x is normform ) implies X is WN )
assume A1: for x being Element of X holds x is normform ; :: thesis: X is WN
let x be Element of X; :: according to ABSRED_0:def 14 :: thesis: x is normalizable
A2: x is normform by A1;
thus ex y being Element of X st y is_normform_of x by A2, LemN2; :: according to ABSRED_0:def 13 :: thesis: verum