let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: ( InputVertices S1 is without_pairs & InnerVertices S2 is Relation implies ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) )
assume ( InputVertices S1 is without_pairs & InnerVertices S2 is Relation ) ; :: thesis: ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
then ( S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 ) by CIRCCOMB:47;
hence ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) by Th4; :: thesis: verum