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

x <=*=> z

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

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

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

A3: x <=*=> y by A1, Lem1A;

thus x <=*=> z by A3, A2, Th7; :: thesis: verum

x <=*=> z

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

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

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

A3: x <=*=> y by A1, Lem1A;

thus x <=*=> z by A3, A2, Th7; :: thesis: verum