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, Lem2;
A4: y =*=> z by A2, Lem2;
thus x =*=> z by A3, A4, Th3; :: thesis: verum