dom the ResultSort of G = the carrier' of G by FUNCT_2:def 1;
hence InnerVertices G is non empty Subset of G by RELAT_1:65; :: thesis: verum