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:
thus X is WN :: thesis:

let x be Element of X; :: according to ABSRED_0:def 14 :: thesis:
( 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:

end;

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

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

end;

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