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 )
given u being Element of X such that A2: ( x =*=> u & u <=*= y ) ; :: according to ABSRED_0:def 21 :: thesis: x <=*=> y
A3: ( x <=*=> u & u <=*=> y ) by A2, LemZ;
thus x <=*=> y by A3, Th7; :: thesis: verum