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 S_{1}[ Element of X] means ex x, y being Element of X st

( x is_normform_of c_{1} & y is_normform_of c_{1} & x <> y );

A5: ex x being Element of X st S_{1}[x]
_{1}[x] holds

ex y being Element of X st

( S_{1}[y] & x ==> y )

thus contradiction by A1, A7; :: thesis: verum

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 S

( x is_normform_of c

A5: ex x being Element of X st S

proof

A6:
for x being Element of X st S
consider x being Element of X such that

B1: ( x1 <=*= x & x =*=> x2 ) by A4;

take x ; :: thesis: S_{1}[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;B1: ( x1 <=*= x & x =*=> x2 ) by A4;

take x ; :: thesis: S

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

ex y being Element of X st

( S

proof

A7:
not X is SN
from ABSRED_0:sch 8(A5, A6);
let x be Element of X; :: thesis: ( S_{1}[x] implies ex y being Element of X st

( S_{1}[y] & x ==> y ) )

assume S_{1}[x]
; :: thesis: ex y being Element of X st

( S_{1}[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;

end;( S

assume S

( S

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 )
;

end;

suppose D1:
y0 = x1
; :: thesis: ex y being Element of X st

( S_{1}[y] & x ==> y )

( S

take
y2
; :: thesis: ( S_{1}[y2] & x ==> y2 )

D2: y0 is_normform_of y2 by C4, C5, LemN7;

x2 is_normform_of y2 by C1, C3;

hence S_{1}[y2]
by C1, D1, D2; :: thesis: x ==> y2

thus x ==> y2 by C3; :: thesis: verum

end;D2: y0 is_normform_of y2 by C4, C5, LemN7;

x2 is_normform_of y2 by C1, C3;

hence S

thus x ==> y2 by C3; :: thesis: verum

suppose D3:
y0 <> x1
; :: thesis: ex y being Element of X st

( S_{1}[y] & x ==> y )

( S

take
y1
; :: thesis: ( S_{1}[y1] & x ==> y1 )

D4: y0 is_normform_of y1 by C4, C5, LemN7;

x1 is_normform_of y1 by C1, C2;

hence ( S_{1}[y1] & x ==> y1 )
by C2, D3, D4; :: thesis: verum

end;D4: y0 is_normform_of y1 by C4, C5, LemN7;

x1 is_normform_of y1 by C1, C2;

hence ( S

thus contradiction by A1, A7; :: thesis: verum