let G2 be reverseEdgeDirections of G,E; :: thesis: G2 is c -edge
the_Edges_of G = the_Edges_of G2 by GLIB_007:4;
hence G2 is c -edge by Th19; :: thesis: verum