let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G2 is reverseEdgeDirections of G1, {} )
assume A1: G1 == G2 ; :: thesis: G2 is reverseEdgeDirections of G1, {}
A2: {} c= the_Edges_of G1 by XBOOLE_1:2;
A3: the_Source_of G2 = the_Source_of G1 by A1, GLIB_000:def 34
.= (the_Source_of G1) +* ((the_Target_of G1) | {}) by FUNCT_4:21 ;
A4: the_Target_of G2 = the_Target_of G1 by A1, GLIB_000:def 34
.= (the_Target_of G1) +* ((the_Source_of G1) | {}) by FUNCT_4:21 ;
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A1, GLIB_000:def 34;
hence G2 is reverseEdgeDirections of G1, {} by A2, A3, A4, GLIB_007:def 1; :: thesis: verum