let G2 be _Graph; :: thesis: for G1 being reverseEdgeDirections of G2
for v1, e, v2 being object holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
let G1 be reverseEdgeDirections of G2; :: thesis: for v1, e, v2 being object holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )
let v1, e, v2 be object ; :: thesis: ( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

hereby :: thesis: ( e DJoins v2,v1,G1 implies e DJoins v1,v2,G2 )

assume e DJoins v1,v2,G2 ; :: thesis: e DJoins v2,v1,G1
then ( e in the_Edges_of G2 & (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) by GLIB_000:def 14;
then ( e in the_Edges_of G1 & (the_Target_of G1) . e = v1 & (the_Source_of G1) . e = v2 ) by Th26, Def1;
hence e DJoins v2,v1,G1 by GLIB_000:def 14; :: thesis: verum

end;

assume e DJoins v2,v1,G1 ; :: thesis: e DJoins v1,v2,G2
then ( e in the_Edges_of G1 & (the_Source_of G1) . e = v2 & (the_Target_of G1) . e = v1 ) by GLIB_000:def 14;
then ( e in the_Edges_of G2 & (the_Target_of G2) . e = v2 & (the_Source_of G2) . e = v1 ) by Th26, Def1;
hence e DJoins v1,v2,G2 by GLIB_000:def 14; :: thesis: verum