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 S1[ Element of X] means x >><< c1;
A3: for y, z being Element of X st y <==> z & S1[y] holds
S1[z]
proof
let y, z be Element of X; :: thesis: ( y <==> z & S1[y] implies S1[z] )
assume B1: ( y <==> z & S1[y] ) ; :: thesis: S1[z]
consider u being Element of X such that
B2: ( x =*=> u & u <=*= y ) by B1, DEF2;
per cases ( y ==> z or y <== z ) by B1;
end;
end;
for y, z being Element of X st y <=*=> z & S1[y] holds
S1[z] from ABSRED_0:sch 5(A3);
 hence for y being Element of X st x <=*=> y holds
x >><< y ; :: thesis: verum