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 y ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> y & y <=*= y )
thus ( x =*=> y & y <=*= y ) by A1, Lem2; :: thesis: verum