let H be DLGraphComplement of G; :: thesis: H is c -vertex
the_Vertices_of G = the_Vertices_of H by GLIB_012:def 6;
hence H is c -vertex by Th18; :: thesis: verum