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