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