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