let X be ARS ; :: thesis: ( X is CONF implies X is CR )

assume A1: X is CONF ; :: thesis: X is CR

let x be Element of X; :: according to ABSRED_0:def 26 :: thesis: for y being Element of X st x <=*=> y holds

x >><< y

defpred S_{1}[ Element of X] means x >><< c_{1};

A3: for y, z being Element of X st y <==> z & S_{1}[y] holds

S_{1}[z]
_{1}[y] holds

S_{1}[z]
from ABSRED_0:sch 5(A3);

hence for y being Element of X st x <=*=> y holds

x >><< y ; :: thesis: verum

assume A1: X is CONF ; :: thesis: X is CR

let x be Element of X; :: according to ABSRED_0:def 26 :: thesis: for y being Element of X st x <=*=> y holds

x >><< y

defpred S

A3: for y, z being Element of X st y <==> z & S

S

proof

for y, z being Element of X st y <=*=> z & S
let y, z be Element of X; :: thesis: ( y <==> z & S_{1}[y] implies S_{1}[z] )

assume B1: ( y <==> z & S_{1}[y] )
; :: thesis: S_{1}[z]

consider u being Element of X such that

B2: ( x =*=> u & u <=*= y ) by B1, DEF2;

end;assume B1: ( y <==> z & S

consider u being Element of X such that

B2: ( x =*=> u & u <=*= y ) by B1, DEF2;

S

hence for y being Element of X st x <=*=> y holds

x >><< y ; :: thesis: verum