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 )

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

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 A3:
for x being Element of X ex y being Element of X st y is_normform_of x
; :: thesis: X is WN
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;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

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