let X be ARS ; :: thesis:
assume A1: X is SN ; :: thesis:
assume A2: not X is WN ; :: thesis:
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 )

let x be Element of X; :: thesis:
assume x in { x where x is Element of X : not x is normalizable } ; :: thesis:
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:
not y is normalizable by A6, A7, LemN5;
hence y in { x where x is Element of X : not x is normalizable } ; :: thesis:
thus x ==> y by A7; :: thesis:

end;