let X be ARS ; :: thesis: ( X is SN & X is WCR implies X is CR )
assume A1: ( X is SN & X is WCR ) ; :: thesis: X is CR
assume A2: not X is CR ; :: thesis: contradiction
A3: not X is CONF by A2;
consider x1, x2 being Element of X such that
A4: ( x1 <<>> x2 & not x1 >><< x2 ) by A3;
defpred S1[ Element of X] means ex x, y being Element of X st
( x is_normform_of c1 & y is_normform_of c1 & x <> y );
A5: ex x being Element of X st S1[x]
proof
consider x being Element of X such that
B1: ( x1 <=*= x & x =*=> x2 ) by A4;
take x ; :: thesis: S1[x]
consider y1 being Element of X such that
B2: y1 is_normform_of x1 by A1, ThWN1;
consider y2 being Element of X such that
B3: y2 is_normform_of x2 by A1, ThWN1;
take y1 ; :: thesis: ex y being Element of X st
( y1 is_normform_of x & y is_normform_of x & y1 <> y )
take y2 ; :: thesis: ( y1 is_normform_of x & y2 is_normform_of x & y1 <> y2 )
thus y1 is_normform_of x by B1, B2, LemN7; :: thesis: ( y2 is_normform_of x & y1 <> y2 )
thus y2 is_normform_of x by B1, B3, LemN7; :: thesis: y1 <> y2
assume B4: y1 = y2 ; :: thesis: contradiction
thus contradiction by A4, B2, B3, B4; :: thesis: verum
end;
A6: for x being Element of X st S1[x] holds
ex y being Element of X st
( S1[y] & x ==> y )
proof
let x be Element of X; :: thesis: ( S1[x] implies ex y being Element of X st
( S1[y] & x ==> y ) )
assume S1[x] ; :: thesis: ex y being Element of X st
( S1[y] & x ==> y )
then consider x1, x2 being Element of X such that
C1: ( x1 is_normform_of x & x2 is_normform_of x & x1 <> x2 ) ;
x =+=> x1 by C1, Lem21;
then consider y1 being Element of X such that
C2: ( x ==> y1 & y1 =*=> x1 ) ;
x =+=> x2 by C1, Lem21;
then consider y2 being Element of X such that
C3: ( x ==> y2 & y2 =*=> x2 ) ;
y1 >><< y2 by A1, C2, C3, Lm11;
then consider y being Element of X such that
C4: ( y1 =*=> y & y <=*= y2 ) ;
consider y0 being Element of X such that
C5: y0 is_normform_of y by A1, ThWN1;
per cases ( y0 = x1 or y0 <> x1 ) ;
suppose D1: y0 = x1 ; :: thesis: ex y being Element of X st
( S1[y] & x ==> y )
take y2 ; :: thesis: ( S1[y2] & x ==> y2 )
D2: y0 is_normform_of y2 by C4, C5, LemN7;
x2 is_normform_of y2 by C1, C3;
hence S1[y2] by C1, D1, D2; :: thesis: x ==> y2
thus x ==> y2 by C3; :: thesis: verum
end;
suppose D3: y0 <> x1 ; :: thesis: ex y being Element of X st
( S1[y] & x ==> y )
take y1 ; :: thesis: ( S1[y1] & x ==> y1 )
D4: y0 is_normform_of y1 by C4, C5, LemN7;
x1 is_normform_of y1 by C1, C2;
hence ( S1[y1] & x ==> y1 ) by C2, D3, D4; :: thesis: verum
end;
end;
end;
A7: not X is SN from ABSRED_0:sch 8(A5, A6);
 thus contradiction by A1, A7; :: thesis: verum