theorem Th11: :: CIRCCOMB:11

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