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

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

suppose A1: E c= the_Edges_of G2 ; :: thesis: G2 is reverseEdgeDirections of G1,E

then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = (the_Source_of G2) +* ((the_Target_of G2) | E) & the_Target_of G1 = (the_Target_of G2) +* ((the_Source_of G2) | E) ) by Def1;
set S1 = the_Source_of G1;
set S2 = the_Source_of G2;
set T1 = the_Target_of G1;
set T2 = the_Target_of G2;
A3: ( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Source_of G2) = the_Edges_of G2 & dom (the_Target_of G2) = the_Edges_of G2 ) by FUNCT_2:def 1;
A4: dom ((the_Source_of G2) | E) = E by A3, A1, RELAT_1:62;
A5: dom ((the_Target_of G2) | E) = E by A3, A1, RELAT_1:62;
A6: the_Source_of G2 = (the_Source_of G2) +* ((the_Source_of G2) | E) by FUNCT_4:75
.= ((the_Source_of G2) +* ((the_Target_of G2) | E)) +* ((the_Source_of G2) | E) by A4, A5, FUNCT_4:74
.= (the_Source_of G1) +* ((the_Target_of G1) | E) by A2, A4 ;
the_Target_of G2 = (the_Target_of G2) +* ((the_Target_of G2) | E) by FUNCT_4:75
.= ((the_Target_of G2) +* ((the_Source_of G2) | E)) +* ((the_Target_of G2) | E) by A4, A5, FUNCT_4:74
.= (the_Target_of G1) +* ((the_Source_of G1) | E) by A2, A5 ;
hence G2 is reverseEdgeDirections of G1,E by A1, A2, A6, Def1; :: thesis: verum

end;

suppose A7: not E c= the_Edges_of G2 ; :: thesis: G2 is reverseEdgeDirections of G1,E

then A8: G1 == G2 by Def1;
then the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
hence G2 is reverseEdgeDirections of G1,E by A7, A8, Def1; :: thesis: verum

end;

end;