let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is _finite
( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G ) by Th4;
hence G1 is _finite by GLIB_000:def 17; :: thesis: verum