theorem :: CIRCTRM1:29

for S1, S2, S3 being non empty ManySortedSign st S1,S2 are_equivalent & S2,S3 are_equivalent holds
S1,S3 are_equivalent