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

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