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

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