theorem Th5: :: CIRCCOMB:5

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
S1 +* S2 = S2 +* S1