theorem Th21: :: FACIRC_2:21

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