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
consider z being Element of X such that
A2: ( x <==> z & z <=*=> y ) by A1;
A3: x <=*=> z by A2, Th6;
thus x <=*=> y by A2, A3, Th7; :: thesis: verum