let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )
S1 tolerates S2 by CIRCCOMB:47;
then ( InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) & InnerVertices (S2 +* S1) = (InnerVertices S2) \/ (InnerVertices S1) ) by CIRCCOMB:11;
hence for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) ) by XBOOLE_0:def 3; :: thesis: verum