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_{1}[ Element of X] means x >><< c_{1};

A4: S_{1}[x]
;

A5: for u, v being Element of X st u <==> v & S_{1}[u] holds

S_{1}[v]
_{1}[y]
from ABSRED_0:sch 6(A2, A4, A5);

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

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

A4: S

A5: for u, v being Element of X st u <==> v & S

S

proof

S
let u, v be Element of X; :: thesis: ( u <==> v & S_{1}[u] implies S_{1}[v] )

assume A6: u <==> v ; :: thesis: ( not S_{1}[u] or S_{1}[v] )

given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S_{1}[v]

end;assume A6: u <==> v ; :: thesis: ( not S

given w being Element of X such that A7: ( x =*=> w & w <=*= u ) ; :: according to ABSRED_0:def 21 :: thesis: S

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

end;

suppose
u ==> v
; :: thesis: S_{1}[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_{1}[v]
by A9, A10, DEF2; :: thesis: verum

end;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

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