let G1 be _Graph; :: thesis:
let E be set ; :: thesis:
let G2 be reverseEdgeDirections of G1,E; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & E c= the_Edges_of G1 ) ; :: thesis:

now :: thesis:

let e be object ; :: thesis:
A2: e is set by TARSKI:1;

hereby :: thesis:

assume e in v2 .edgesIn() ; :: thesis:
then consider x being set such that
A3: e DJoins x,v2,G2 by GLIB_000:57;

per cases ;

suppose A4: e in E ; :: thesis:

then e DJoins v2,x,G1 by A1, A3, GLIB_007:7;
then e in v1 .edgesOut() by A1, A2, GLIB_000:59;
then e in (v1 .edgesOut()) /\ E by A4, XBOOLE_0:def 4;
hence e in ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) by XBOOLE_0:def 3; :: thesis:

end;

suppose A5: not e in E ; :: thesis:

then e DJoins x,v2,G1 by A1, A3, GLIB_007:8;
then e in v1 .edgesIn() by A1, A2, GLIB_000:57;
then e in (v1 .edgesIn()) \ E by A5, XBOOLE_0:def 5;
hence e in ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume e in ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose e in (v1 .edgesIn()) \ E ; :: thesis:

then A6: ( e in v1 .edgesIn() & not e in E ) by XBOOLE_0:def 5;
then consider x being set such that
A7: e DJoins x,v1,G1 by GLIB_000:57;
e DJoins x,v1,G2 by A1, A6, A7, GLIB_007:8;
hence e in v2 .edgesIn() by A1, A2, GLIB_000:57; :: thesis:

end;

suppose e in (v1 .edgesOut()) /\ E ; :: thesis:

then A8: ( e in v1 .edgesOut() & e in E ) by XBOOLE_0:def 4;
then consider x being set such that
A9: e DJoins v1,x,G1 by GLIB_000:59;
e DJoins x,v1,G2 by A1, A8, A9, GLIB_007:7;
hence e in v2 .edgesIn() by A1, A2, GLIB_000:57; :: thesis:

end;

end;

end;

hence v2 .edgesIn() = ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) by TARSKI:2; :: thesis:

now :: thesis:

let e be object ; :: thesis:
A10: e is set by TARSKI:1;

hereby :: thesis:

assume e in v2 .edgesOut() ; :: thesis:
then consider x being set such that
A11: e DJoins v2,x,G2 by GLIB_000:59;

per cases ;

suppose A12: e in E ; :: thesis:

then e DJoins x,v2,G1 by A1, A11, GLIB_007:7;
then e in v1 .edgesIn() by A1, A10, GLIB_000:57;
then e in (v1 .edgesIn()) /\ E by A12, XBOOLE_0:def 4;
hence e in ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) by XBOOLE_0:def 3; :: thesis:

end;

suppose A13: not e in E ; :: thesis:

then e DJoins v2,x,G1 by A1, A11, GLIB_007:8;
then e in v1 .edgesOut() by A1, A10, GLIB_000:59;
then e in (v1 .edgesOut()) \ E by A13, XBOOLE_0:def 5;
hence e in ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume e in ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose e in (v1 .edgesOut()) \ E ; :: thesis:

then A14: ( e in v1 .edgesOut() & not e in E ) by XBOOLE_0:def 5;
then consider x being set such that
A15: e DJoins v1,x,G1 by GLIB_000:59;
e DJoins v1,x,G2 by A1, A14, A15, GLIB_007:8;
hence e in v2 .edgesOut() by A1, A10, GLIB_000:59; :: thesis:

end;

suppose e in (v1 .edgesIn()) /\ E ; :: thesis:

then A16: ( e in v1 .edgesIn() & e in E ) by XBOOLE_0:def 4;
then consider x being set such that
A17: e DJoins x,v1,G1 by GLIB_000:57;
e DJoins v1,x,G2 by A1, A16, A17, GLIB_007:7;
hence e in v2 .edgesOut() by A1, A10, GLIB_000:59; :: thesis:

end;

end;

end;

hence v2 .edgesOut() = ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) by TARSKI:2; :: thesis: