let G2 be _trivial _Graph; :: thesis: for E being set
for G1 being _Graph holds
( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )
let E be set ; :: thesis: for G1 being _Graph holds
( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )
let G1 be _Graph; :: thesis: ( G1 == G2 iff G1 is reverseEdgeDirections of G2,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: ( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )

consider v being Vertex of G2 such that
the_Vertices_of G2 = {v} and
A2: ( the_Source_of G2 = (the_Edges_of G2) --> v & the_Target_of G2 = (the_Edges_of G2) --> v ) by GLIB_000:106;
A3: (the_Source_of G2) +* ((the_Target_of G2) | E) = (the_Edges_of G2) --> v by A2, FUNCT_4:75;

hereby :: thesis: ( G1 is reverseEdgeDirections of G2,E implies G1 == G2 )

assume G1 == G2 ; :: thesis: G1 is reverseEdgeDirections of G2,E
then ( 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 G1 = the_Target_of G2 ) by GLIB_000:def 34;
hence G1 is reverseEdgeDirections of G2,E by A1, A2, A3, Def1; :: thesis: verum

end;

assume G1 is reverseEdgeDirections of G2,E ; :: thesis: G1 == G2
then ( 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 A1, Def1;
hence G1 == G2 by A2, A3, GLIB_000:def 34; :: thesis: verum

end;

suppose not E c= the_Edges_of G2 ; :: thesis: ( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )

hence ( G1 == G2 iff G1 is reverseEdgeDirections of G2,E ) by Def1; :: thesis: verum

end;

end;