let G2 be _Graph; :: thesis: for E, V being set
for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V
let E, V be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V
let G1 be reverseEdgeDirections of G2,E; :: thesis: G1 .edgesBetween V = G2 .edgesBetween V
for e being object holds
( e in G1 .edgesBetween V iff e in G2 .edgesBetween V )

proof

let e be object ; :: thesis: ( e in G1 .edgesBetween V iff e in G2 .edgesBetween V )
set x1 = (the_Source_of G1) . e;
set y1 = (the_Target_of G1) . e;
set x2 = (the_Source_of G2) . e;
set y2 = (the_Target_of G2) . e;

hereby :: thesis: ( e in G2 .edgesBetween V implies e in G1 .edgesBetween V )

assume A1: e in G1 .edgesBetween V ; :: thesis: e in G2 .edgesBetween V
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G2 by Th9;
then ( e in the_Edges_of G2 & ( ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) or ( (the_Source_of G1) . e = (the_Target_of G2) . e & (the_Target_of G1) . e = (the_Source_of G2) . e ) ) ) by GLIB_000:def 13;
then ( e in the_Edges_of G2 & (the_Source_of G2) . e in V & (the_Target_of G2) . e in V ) by A1, GLIB_000:31;
hence e in G2 .edgesBetween V by GLIB_000:31; :: thesis: verum

end;

assume A2: e in G2 .edgesBetween V ; :: thesis: e in G1 .edgesBetween V
then e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:def 13;
then e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G1 by Th9;
then ( e in the_Edges_of G1 & ( ( (the_Source_of G1) . e = (the_Source_of G2) . e & (the_Target_of G1) . e = (the_Target_of G2) . e ) or ( (the_Source_of G1) . e = (the_Target_of G2) . e & (the_Target_of G1) . e = (the_Source_of G2) . e ) ) ) by GLIB_000:def 13;
then ( e in the_Edges_of G1 & (the_Source_of G1) . e in V & (the_Target_of G1) . e in V ) by A2, GLIB_000:31;
hence e in G1 .edgesBetween V by GLIB_000:31; :: thesis: verum

end;

hence G1 .edgesBetween V = G2 .edgesBetween V by TARSKI:2; :: thesis: verum