defpred S1[ 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 S1[x,y] ) from reconsider z = 0 , o = 1 as Element of X by ;
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 ;
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 ; :: thesis: verum
end;
hence not X is SN by ; :: thesis: verum