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, Th2;

thus x =*=> y by A2, A3, Th3; :: thesis: verum

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, Th2;

thus x =*=> y by A2, A3, Th3; :: thesis: verum