theorem Th21: :: FACIRC_1:21

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign
for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )