theorem Th6: :: FACIRC_1:6

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InnerVertices S2 is Relation holds
( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )