let X be ARS ; :: thesis: ( X is DIAMOND implies X is CR )
assume A1: X is DIAMOND ; :: 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
let y be Element of X; :: thesis: ( x <=*=> y implies x >><< y )
assume A2: x <=*=> y ; :: thesis: x >><< y
defpred S₁[ Element of X] means x >><< c₁;
A4: S₁[x] ;
A5: for u, v being Element of X st u <==> v & S₁[u] holds
S₁[v]

proof

let u, v be Element of X; :: thesis: ( u <==> v & S₁[u] implies S₁[v] )
assume A6: u <==> v ; :: thesis: ( not S₁[u] or S₁[v] )
given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S₁[v]

per cases ( u ==> v or u <== v ) by A6;

suppose u ==> v ; :: thesis: S₁[v]

then A8: u =01=> v ;
consider a being Element of X such that
A9: ( w =01=> a & a <=*= v ) by A1, A7, A8, LemA;
A10: x =*=> a by A7, A9, Lem11;
thus S₁[v] by A9, A10, DEF2; :: thesis: verum

end;

suppose u <== v ; :: thesis: S₁[v]

then A11: v =*=> w by A7, Lem5;
thus S₁[v] by A7, A11, DEF2; :: thesis: verum

end;

end;

end;

S₁[y] from ABSRED_0:sch 6(A2, A4, A5);
hence x >><< y ; :: thesis: verum