let X be ARS ; :: thesis: for x, y, z being Element of X st x =*=> y & y =+=> z holds
x =+=> z
let x, y, z be Element of X; :: thesis: ( x =*=> y & y =+=> z implies x =+=> z )
assume A1: x =*=> y ; :: thesis: ( not y =+=> z or x =+=> z )
assume A2: y =+=> z ; :: thesis: x =+=> z
consider u being Element of X such that
A3: ( y =*=> u & u ==> z ) by A2, Th4;
thus x =+=> z by A3, A1, Th3, Th4; :: thesis: verum