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

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