let X be ARS ; :: thesis: for u, x, y, z being Element of X st x ==> y & y =+=> z & z ==> u holds
x =+=> u
let u, x, y, z be Element of X; :: thesis: ( x ==> y & y =+=> z & z ==> u implies x =+=> u )
assume A1: x ==> y ; :: thesis: ( not y =+=> z or not z ==> u or x =+=> u )
assume A2: y =+=> z ; :: thesis: ( not z ==> u or x =+=> u )
assume A3: z ==> u ; :: thesis: x =+=> u
A4: x =*=> z by A1, A2, Lem5A;
thus x =+=> u by A3, A4, Th4; :: thesis: verum