let X be ARS ; :: thesis: for x, y, z being Element of X st x ==> y & y =01=> z holds

x =*=> z

let x, y, z be Element of X; :: thesis: ( x ==> y & y =01=> z implies x =*=> z )

assume A1: x ==> y ; :: thesis: ( not y =01=> z or x =*=> z )

assume A2: y =01=> z ; :: thesis: x =*=> z

A3: x =*=> y by A1, Th2;

A4: y =*=> z by A2, Lem1;

thus x =*=> z by A3, A4, Th3; :: thesis: verum

x =*=> z

let x, y, z be Element of X; :: thesis: ( x ==> y & y =01=> z implies x =*=> z )

assume A1: x ==> y ; :: thesis: ( not y =01=> z or x =*=> z )

assume A2: y =01=> z ; :: thesis: x =*=> z

A3: x =*=> y by A1, Th2;

A4: y =*=> z by A2, Lem1;

thus x =*=> z by A3, A4, Th3; :: thesis: verum