let X be ARS ; :: thesis: for x, y being Element of X st x =+=> y holds
x <<>> y
let x, y be Element of X; :: thesis: ( x =+=> y implies x <<>> y )
assume A1: x =+=> y ; :: thesis: x <<>> y
take x ; :: according to ABSRED_0:def 20 :: thesis: ( x <=*= x & x =*=> y )
thus ( x <=*= x & x =*=> y ) by A1, Lem2; :: thesis: verum