let G2 be reverseEdgeDirections of G,E; :: thesis: G2 is c -vertex
the_Vertices_of G = the_Vertices_of G2 by GLIB_007:4;
hence G2 is c -vertex by Th18; :: thesis: verum