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, Lem2A;
A4: y <==> z by A2;
thus x <=+=> z by A3, A4, Def8; :: thesis: verum