let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is _trivial
A1: the_Vertices_of G1 = the_Vertices_of G by Th4;
card (the_Vertices_of G) = 1 by GLIB_000:def 19;
hence G1 is _trivial by A1, GLIB_000:def 19; :: thesis: verum