theorem Th5: :: CIRCCMB2:5

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1))