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