defpred S₁[ set , set ] means $1 = 0 ;
consider X being non empty strict ARS such that
A1: the carrier of X = {0,1} and
A2: for x, y being Element of X holds
( x ==> y iff S₁[x,y] ) from ABSRED_0:sch 7();
reconsider z = 0 , o = 1 as Element of X by A1, TARSKI:def 2;
A3: z <> o ;
take X ; :: thesis: ( X is WN & not X is SN )
thus X is WN :: thesis: not X is SN

proof

let x be Element of X; :: according to ABSRED_0:def 14 :: thesis: x is normalizable
( x = 0 or x = 1 ) by A1, TARSKI:def 2;
then ( x is normform or x is normalizable ) by A2, A3, LmA;
hence x is normalizable ; :: thesis: verum

end;

set A = {z};
A4: z in {z} by TARSKI:def 1;

now :: thesis: for x being Element of X st x in {z} holds
ex y being Element of X st
( y in {z} & x ==> y )

let x be Element of X; :: thesis: ( x in {z} implies ex y being Element of X st
( y in {z} & x ==> y ) )
assume x in {z} ; :: thesis: ex y being Element of X st
( y in {z} & x ==> y )
then A5: x = z by TARSKI:def 1;
take y = z; :: thesis: ( y in {z} & x ==> y )
thus ( y in {z} & x ==> y ) by A2, A5, TARSKI:def 1; :: thesis: verum

end;

hence not X is SN by A4, ThSN; :: thesis: verum