theorem Th3: :: CIRCCOMB:3
for S1, S2, S3 being non empty ManySortedSign st S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1 holds
S1 +* S2 tolerates S3