let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; :: thesis: ( not InputVertices S1 is with_pair & InnerVertices S1 is Relation & not InputVertices S2 is with_pair & InnerVertices S2 is Relation implies InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2) )
assume A1: ( not InputVertices S1 is with_pair & InnerVertices S1 is Relation & not InputVertices S2 is with_pair & InnerVertices S2 is Relation ) ; :: thesis: InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)
then A2: InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) by Th6;
InnerVertices S1 misses InputVertices S2 by A1, Th5;
hence InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2) by A2, XBOOLE_1:83; :: thesis: verum