theorem :: FACIRC_1:3

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation by Th2, CIRCCOMB:47;