let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds
e DJoins v2,v1,G1
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds
e DJoins v2,v1,G1
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds
e DJoins v2,v1,G1
let v1, e, v2 be object ; :: thesis: ( E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 implies e DJoins v2,v1,G1 )
assume A1: ( E c= the_Edges_of G2 & e in E ) ; :: thesis: ( not e DJoins v1,v2,G2 or e DJoins v2,v1,G1 )
set S1 = the_Source_of G1;
set T1 = the_Target_of G1;
set S2 = the_Source_of G2;
set T2 = the_Target_of G2;
assume e DJoins v1,v2,G2 ; :: thesis: e DJoins v2,v1,G1
then A2: ( e in the_Edges_of G2 & (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) by GLIB_000:def 14;
( E c= dom (the_Source_of G2) & E c= dom (the_Target_of G2) ) by A1, FUNCT_2:def 1;
then A3: ( e in dom ((the_Source_of G2) | E) & e in dom ((the_Target_of G2) | E) ) by A1, RELAT_1:62;
A4: (the_Source_of G1) . e = ((the_Source_of G2) +* ((the_Target_of G2) | E)) . e by A1, Def1
.= ((the_Target_of G2) | E) . e by A3, FUNCT_4:13
.= v2 by A2, A3, FUNCT_1:47 ;
A5: (the_Target_of G1) . e = ((the_Target_of G2) +* ((the_Source_of G2) | E)) . e by A1, Def1
.= ((the_Source_of G2) | E) . e by A3, FUNCT_4:13
.= v1 by A2, A3, FUNCT_1:47 ;
e in the_Edges_of G1 by A2, Th4;
hence e DJoins v2,v1,G1 by A4, A5, GLIB_000:def 14; :: thesis: verum