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