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