let X be ARS ; :: thesis: ( not X is CONF & X is WN implies ex x, y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z ) )
given a, b being Element of X such that A1: ( a <<>> b & not a >><< b ) ; :: according to ABSRED_0:def 25 :: thesis: ( not X is WN or ex x, y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z ) )
consider x being Element of X such that
A0: ( a <=*= x & x =*=> b ) by A1;
assume A2: for c being Element of X holds c is normalizable ; :: according to ABSRED_0:def 14 :: thesis: ex x, y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z )
then a is normalizable ;
then consider y being Element of X such that
A3: y is_normform_of a ;
b is normalizable by A2;
then consider z being Element of X such that
A4: z is_normform_of b ;
take x ; :: thesis: ex y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z )
take y ; :: thesis: ex z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z )
take z ; :: thesis: ( y is_normform_of x & z is_normform_of x & y <> z )
thus ( y is_normform_of x & z is_normform_of x ) by A0, A3, A4, LemN7; :: thesis: y <> z
thus y <> z by A1, A3, A4; :: thesis: verum