theorem Th4: :: YELLOW18:4
for A, B, C being category st A,B are_equivalent & B,C are_equivalent holds
A,C are_equivalent