for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds v is Vertex of (S1 +* S2)