theorem :: CIRCCMB3:24

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