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 )

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

thus
contradiction
by A1, A4, A5, ThSN; :: thesis: verum
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;( 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