let U1, U2, U3 be Universal_Algebra; :: thesis: ( U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar )
assume ( U1,U2 are_similar & U2,U3 are_similar ) ; :: thesis: U1,U3 are_similar
then ( signature U1 = signature U2 & signature U2 = signature U3 ) by Def2;
hence U1,U3 are_similar by Def2; :: thesis: verum