theorem Th8: :: FACIRC_1:8

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