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: y <=01=> z by A2, Lem43;

thus x <=+=> z by A1, A3, Lem18; :: 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: y <=01=> z by A2, Lem43;

thus x <=+=> z by A1, A3, Lem18; :: thesis: verum