let G be _Graph; :: thesis: for E being set
for G1, G2 being reverseEdgeDirections of G,E holds G1 == G2
let E be set ; :: thesis: for G1, G2 being reverseEdgeDirections of G,E holds G1 == G2
let G1, G2 be reverseEdgeDirections of G,E; :: thesis: G1 == G2

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

suppose A1: E c= the_Edges_of G ; :: thesis: G1 == G2

A2: ( 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 A1, Def1;
( 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, Def1;
hence G1 == G2 by A2, GLIB_000:def 34; :: thesis: verum

end;

suppose not E c= the_Edges_of G ; :: thesis: G1 == G2

then ( G1 == G & G2 == G ) by Def1;
hence G1 == G2 by GLIB_000:85; :: thesis: verum

end;

end;