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 ( 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 ( InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) & InnerVertices S1 misses InputVertices S2 ) by Th5, Th6;
hence InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2) by XBOOLE_1:83; :: thesis: verum