let H be DGraphComplement of G; :: thesis: H is c -vertex
the_Vertices_of G = the_Vertices_of H by GLIB_012:80;
hence H is c -vertex by Th18; :: thesis: verum