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

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