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 S1[ Element of X] means x >><< c1;
A4: S1[x] ;
A5: for u, v being Element of X st u <==> v & S1[u] holds
S1[v]
proof
let u, v be Element of X; :: thesis: ( u <==> v & S1[u] implies S1[v] )
assume A6: u <==> v ; :: thesis: ( not S1[u] or S1[v] )
given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S1[v]
per cases ( u ==> v or u <== v ) by A6;
suppose u ==> v ; :: thesis: S1[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 S1[v] by A9, A10, DEF2; :: thesis: verum
end;
end;
end;
S1[y] from ABSRED_0:sch 6(A2, A4, A5);
hence x >><< y ; :: thesis: verum