let X be ARS ; :: thesis: ( X is CR implies X is WCR )
assume A1: X is CR ; :: thesis: X is WCR
let x be Element of X; :: according to ABSRED_0:def 27 :: thesis: for y being Element of X st x <<01>> y holds
x >><< y
let y be Element of X; :: thesis: ( x <<01>> y implies x >><< y )
assume A2: x <<01>> y ; :: thesis: x >><< y
A4: x <=*=> y by A2, Lem18, Lem19;
thus x >><< y by A1, A4; :: thesis: verum