theorem Th13: :: CIRCCOMB:13

for S1, S2 being non empty ManySortedSign st S1 tolerates S2 holds
for v1 being Vertex of S1 st v1 in InputVertices (S1 +* S2) holds
v1 in InputVertices S1