let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
S1 tolerates S2 by CIRCCOMB:47;
hence InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:11; :: thesis: verum