let X be ARS ; :: thesis: for x, y, z being Element of X st x <=01=> y & y <=+=> z holds
x <=+=> z
let x, y, z be Element of X; :: thesis: ( x <=01=> y & y <=+=> z implies x <=+=> z )
assume A1: x <=01=> 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, Th8;
thus x <=+=> z by A3, A1, Lm8, Th8; :: thesis: verum