let S1, S2 be non empty ManySortedSign ; :: thesis: for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2)
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
InnerVertices (S1 +* S2) = rng (the ResultSort of S1 +* the ResultSort of S2) by CIRCCOMB:def 2;
then InnerVertices S2 c= InnerVertices (S1 +* S2) by FUNCT_4:19;
hence for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2) ; :: thesis: verum