let G2, G3 be _Graph; :: thesis: for v, e, w being object
for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
let v, e, w be object ; :: thesis: for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
let G1 be addEdge of G3,v,e,w; :: thesis: ( not e in the_Edges_of G3 implies ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v ) )
assume A1: not e in the_Edges_of G3 ; :: thesis: ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )

per cases ( ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) or not v in the_Vertices_of G3 or not w in the_Vertices_of G3 ) ;

suppose A2: ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) ; :: thesis: ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )

then the_Edges_of G1 = (the_Edges_of G3) \/ {e} by A1, GLIB_006:def 11;
then A3: {e} c= the_Edges_of G1 by XBOOLE_1:7;
( dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Target_of G1) = the_Edges_of G1 ) by FUNCT_2:def 1;
then A4: ( e in dom (the_Source_of G1) & e in dom (the_Target_of G1) & e is set ) by A3, ZFMISC_1:31, TARSKI:1;
set S = the_Source_of G3;
set T = the_Target_of G3;

hereby :: thesis: ( G2 is addEdge of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )

assume A5: G2 is reverseEdgeDirections of G1,{e} ; :: thesis: G2 is addEdge of G3,w,e,v
then A6: the_Vertices_of G2 = the_Vertices_of G1 by A3, GLIB_007:def 1
.= the_Vertices_of G3 by A2, GLIB_006:102 ;

now :: thesis: for e0, v0, w0 being object st e0 DJoins v0,w0,G3 holds
e0 DJoins v0,w0,G2

let e0, v0, w0 be object ; :: thesis: ( e0 DJoins v0,w0,G3 implies e0 DJoins v0,w0,G2 )
assume A7: e0 DJoins v0,w0,G3 ; :: thesis: e0 DJoins v0,w0,G2
then e0 in the_Edges_of G3 by GLIB_000:def 14;
then A8: not e0 in {e} by A1, TARSKI:def 1;
( v0 is set & w0 is set ) by TARSKI:1;
then e0 DJoins v0,w0,G1 by A7, GLIB_006:70;
hence e0 DJoins v0,w0,G2 by A3, A5, A8, GLIB_007:8; :: thesis: verum

end;

then A9: G2 is Supergraph of G3 by A6, Th50;
A10: the_Edges_of G2 = the_Edges_of G1 by A3, A5, GLIB_007:def 1
.= (the_Edges_of G3) \/ {e} by A1, A2, GLIB_006:def 11 ;
A11: the_Source_of G2 = (the_Source_of G1) +* ((the_Target_of G1) | {e}) by A5, A3, GLIB_007:def 1
.= (the_Source_of G1) +* (e .--> ((the_Target_of G1) . e)) by A4, FUNCT_7:6
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> ((the_Target_of G1) . e)) by A1, A2, GLIB_006:def 11
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> (((the_Target_of G3) +* (e .--> w)) . e)) by A1, A2, GLIB_006:def 11
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> w) by FUNCT_4:113
.= (the_Source_of G3) +* (e .--> w) by FUNCT_4:114 ;
the_Target_of G2 = (the_Target_of G1) +* ((the_Source_of G1) | {e}) by A5, A3, GLIB_007:def 1
.= (the_Target_of G1) +* (e .--> ((the_Source_of G1) . e)) by A4, FUNCT_7:6
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> ((the_Source_of G1) . e)) by A1, A2, GLIB_006:def 11
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> (((the_Source_of G3) +* (e .--> v)) . e)) by A1, A2, GLIB_006:def 11
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> v) by FUNCT_4:113
.= (the_Target_of G3) +* (e .--> v) by FUNCT_4:114 ;
hence G2 is addEdge of G3,w,e,v by A1, A2, A6, A9, A10, A11, GLIB_006:def 11; :: thesis: verum

end;

assume A12: G2 is addEdge of G3,w,e,v ; :: thesis: G2 is reverseEdgeDirections of G1,{e}
then A13: the_Vertices_of G2 = the_Vertices_of G3 by A2, GLIB_006:102
.= the_Vertices_of G1 by A2, GLIB_006:102 ;
A14: the_Edges_of G2 = (the_Edges_of G3) \/ {e} by A1, A2, A12, GLIB_006:def 11
.= the_Edges_of G1 by A1, A2, GLIB_006:def 11 ;
A15: the_Source_of G2 = (the_Source_of G3) +* (e .--> w) by A1, A2, A12, GLIB_006:def 11
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> w) by FUNCT_4:114
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> (((the_Target_of G3) +* (e .--> w)) . e)) by FUNCT_4:113
.= ((the_Source_of G3) +* (e .--> v)) +* (e .--> ((the_Target_of G1) . e)) by A1, A2, GLIB_006:def 11
.= (the_Source_of G1) +* (e .--> ((the_Target_of G1) . e)) by A1, A2, GLIB_006:def 11
.= (the_Source_of G1) +* ((the_Target_of G1) | {e}) by A4, FUNCT_7:6 ;
the_Target_of G2 = (the_Target_of G3) +* (e .--> v) by A1, A2, A12, GLIB_006:def 11
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> v) by FUNCT_4:114
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> (((the_Source_of G3) +* (e .--> v)) . e)) by FUNCT_4:113
.= ((the_Target_of G3) +* (e .--> w)) +* (e .--> ((the_Source_of G1) . e)) by A1, A2, GLIB_006:def 11
.= (the_Target_of G1) +* (e .--> ((the_Source_of G1) . e)) by A1, A2, GLIB_006:def 11
.= (the_Target_of G1) +* ((the_Source_of G1) | {e}) by A4, FUNCT_7:6 ;
hence G2 is reverseEdgeDirections of G1,{e} by A3, A13, A14, A15, GLIB_007:def 1; :: thesis: verum

end;

suppose A16: ( not v in the_Vertices_of G3 or not w in the_Vertices_of G3 ) ; :: thesis: ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )

then A17: G1 == G3 by GLIB_006:def 11;
then the_Edges_of G1 = the_Edges_of G3 by GLIB_000:def 34;
then A18: not {e} c= the_Edges_of G1 by A1, ZFMISC_1:31;

hereby :: thesis: ( G2 is addEdge of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )

assume G2 is reverseEdgeDirections of G1,{e} ; :: thesis: G2 is addEdge of G3,w,e,v
then G2 == G1 by A18, GLIB_007:def 1;
then A19: G2 == G3 by A17, GLIB_000:85;
then G2 is Supergraph of G3 by GLIB_006:59;
hence G2 is addEdge of G3,w,e,v by A16, A19, GLIB_006:def 11; :: thesis: verum

end;

assume G2 is addEdge of G3,w,e,v ; :: thesis: G2 is reverseEdgeDirections of G1,{e}
then G2 == G3 by A16, GLIB_006:def 11;
then G2 == G1 by A17, GLIB_000:85;
hence G2 is reverseEdgeDirections of G1,{e} by A18, GLIB_007:def 1; :: thesis: verum

end;

end;