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
A4: y <=*=> z by A2, Lem2A;
thus x <=*=> z by A1, A4, Th7; :: thesis: verum