let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 holds
for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 holds
for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1
let G1 be reverseEdgeDirections of G2,E; :: thesis: ( E c= the_Edges_of G2 implies for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1 )
assume A1: E c= the_Edges_of G2 ; :: thesis: for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1
let v1, e, v2 be object ; :: thesis: ( e Joins v1,v2,G2 implies e Joins v1,v2,G1 )
assume A2: e Joins v1,v2,G2 ; :: thesis: e Joins v1,v2,G1

per cases ( e in E or not e in E ) ;

suppose A3: e in E ; :: thesis: e Joins v1,v2,G1

then A4: e in the_Edges_of G2 by A1;
then ( e in dom (the_Source_of G2) & e in dom (the_Target_of G2) ) by FUNCT_2:def 1;
then A5: ( e in dom ((the_Source_of G2) | E) & e in dom ((the_Target_of G2) | E) ) by A3, RELAT_1:57;
A6: (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 A5, FUNCT_4:13
.= (the_Target_of G2) . e by A3, FUNCT_1:49 ;
A7: (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 A5, FUNCT_4:13
.= (the_Source_of G2) . e by A3, FUNCT_1:49 ;
A8: e in the_Edges_of G1 by A4, Th4;

per cases ( ( (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) or ( (the_Source_of G2) . e = v2 & (the_Target_of G2) . e = v1 ) ) by A2, GLIB_000:def 13;

suppose ( (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) ; :: thesis: e Joins v1,v2,G1

hence e Joins v1,v2,G1 by A6, A7, A8, GLIB_000:def 13; :: thesis: verum

end;

suppose ( (the_Source_of G2) . e = v2 & (the_Target_of G2) . e = v1 ) ; :: thesis: e Joins v1,v2,G1

hence e Joins v1,v2,G1 by A6, A7, A8, GLIB_000:def 13; :: thesis: verum

end;

end;

end;

suppose A9: not e in E ; :: thesis: e Joins v1,v2,G1

then A10: not e in dom ((the_Target_of G2) | E) ;
A11: (the_Source_of G1) . e = ((the_Source_of G2) +* ((the_Target_of G2) | E)) . e by A1, Def1
.= (the_Source_of G2) . e by A10, FUNCT_4:11 ;
A12: not e in dom ((the_Source_of G2) | E) by A9;
A13: (the_Target_of G1) . e = ((the_Target_of G2) +* ((the_Source_of G2) | E)) . e by A1, Def1
.= (the_Target_of G2) . e by A12, FUNCT_4:11 ;
e in the_Edges_of G2 by A2, GLIB_000:def 13;
then A14: e in the_Edges_of G1 by Th4;

per cases ( ( (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) or ( (the_Source_of G2) . e = v2 & (the_Target_of G2) . e = v1 ) ) by A2, GLIB_000:def 13;

suppose ( (the_Source_of G2) . e = v1 & (the_Target_of G2) . e = v2 ) ; :: thesis: e Joins v1,v2,G1

hence e Joins v1,v2,G1 by A11, A13, A14, GLIB_000:def 13; :: thesis: verum

end;

suppose ( (the_Source_of G2) . e = v2 & (the_Target_of G2) . e = v1 ) ; :: thesis: e Joins v1,v2,G1

hence e Joins v1,v2,G1 by A11, A13, A14, GLIB_000:def 13; :: thesis: verum

end;

end;

end;

end;