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₁[ Element of X] means x >><< c₁;
A3: for y, z being Element of X st y <==> z & S₁[y] holds
S₁[z]

proof

let y, z be Element of X; :: thesis: ( y <==> z & S₁[y] implies S₁[z] )
assume B1: ( y <==> z & S₁[y] ) ; :: thesis: S₁[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;

suppose B3: y ==> z ; :: thesis: S₁[z]

y =*=> z by B3, Th2;
then u <<>> z by B2;
hence S₁[z] by A1, B2, Lm5; :: thesis: verum

end;

suppose B5: y <== z ; :: thesis: S₁[z]

thus S₁[z] by B1, B5, Th2, Lm5; :: thesis: verum

end;

end;

end;

for y, z being Element of X st y <=*=> z & S₁[y] holds
S₁[z] from ABSRED_0:sch 5(A3);
hence for y being Element of X st x <=*=> y holds
x >><< y ; :: thesis: verum