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