let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is loopless
for v, e being object holds not e Joins v,v,G1 by Th9, GLIB_000:18;
hence G1 is loopless by GLIB_000:18; :: thesis: verum