let G, G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G,E st G1 == G2 holds
G2 is reverseEdgeDirections of G,E
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G,E st G1 == G2 holds
G2 is reverseEdgeDirections of G,E
let G1 be reverseEdgeDirections of G,E; :: thesis: ( G1 == G2 implies G2 is reverseEdgeDirections of G,E )
assume A1: G1 == G2 ; :: thesis: G2 is reverseEdgeDirections of G,E

per cases ( E c= the_Edges_of G or not E c= the_Edges_of G ) ;

suppose A2: E c= the_Edges_of G ; :: thesis: G2 is reverseEdgeDirections of G,E

then ( the_Vertices_of G1 = the_Vertices_of G & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of G1 = (the_Target_of G) +* ((the_Source_of G) | E) ) by Def1;
then ( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = the_Edges_of G & the_Source_of G2 = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of G2 = (the_Target_of G) +* ((the_Source_of G) | E) ) by A1, GLIB_000:def 34;
hence G2 is reverseEdgeDirections of G,E by A2, Def1; :: thesis: verum

end;

suppose A3: not E c= the_Edges_of G ; :: thesis: G2 is reverseEdgeDirections of G,E

then G == G1 by Def1;
then G == G2 by A1, GLIB_000:85;
hence G2 is reverseEdgeDirections of G,E by A3, Def1; :: thesis: verum

end;

end;