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