let X be ARS ; :: thesis: ( X is SN implies X is WN )
assume A1: X is SN ; :: thesis: X is WN
assume A2: not X is WN ; :: thesis: contradiction
consider z being Element of X such that
A3: not z is normalizable by A2;
set A = { x where x is Element of X : not x is normalizable } ;
A4: z in { x where x is Element of X : not x is normalizable } by A3;
A5: for x being Element of X st x in { x where x is Element of X : not x is normalizable } holds
ex y being Element of X st
( y in { x where x is Element of X : not x is normalizable } & x ==> y )

proof

let x be Element of X; :: thesis: ( x in { x where x is Element of X : not x is normalizable } implies ex y being Element of X st
( y in { x where x is Element of X : not x is normalizable } & x ==> y ) )
assume x in { x where x is Element of X : not x is normalizable } ; :: thesis: ex y being Element of X st
( y in { x where x is Element of X : not x is normalizable } & x ==> y )
then A6: ex y being Element of X st
( x = y & not y is normalizable ) ;
then not x is normform ;
then consider y being Element of X such that
A7: x ==> y ;
take y ; :: thesis: ( y in { x where x is Element of X : not x is normalizable } & x ==> y )
not y is normalizable by A6, A7, LemN5;
hence y in { x where x is Element of X : not x is normalizable } ; :: thesis: x ==> y
thus x ==> y by A7; :: thesis: verum

end;

thus contradiction by A1, A4, A5, ThSN; :: thesis: verum