let G1 be _Graph; :: thesis:
let G2 be reverseEdgeDirections of G1; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: v1 = v2 ; :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume A2: e in v2 .edgesIn() ; :: thesis:
A3: e is set by TARSKI:1;
consider x being set such that
A4: e DJoins x,v2,G2 by A2, GLIB_000:57;
e in the_Edges_of G2 by A4, GLIB_000:def 14;
then e in the_Edges_of G1 by GLIB_007:4;
then e DJoins v1,x,G1 by A1, A4, GLIB_007:7;
hence e in v1 .edgesOut() by A3, GLIB_000:59; :: thesis:

end;

assume A5: e in v1 .edgesOut() ; :: thesis:
A6: e is set by TARSKI:1;
consider x being set such that
A7: e DJoins v1,x,G1 by A5, GLIB_000:59;
e in the_Edges_of G1 by A7, GLIB_000:def 14;
then e DJoins x,v2,G2 by A1, A7, GLIB_007:7;
hence e in v2 .edgesIn() by A6, GLIB_000:57; :: thesis:

end;

hence v2 .edgesIn() = v1 .edgesOut() by TARSKI:2; :: thesis:
hence v2 .inDegree() = v1 .outDegree() ; :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

assume A8: e in v2 .edgesOut() ; :: thesis:
A9: e is set by TARSKI:1;
consider x being set such that
A10: e DJoins v2,x,G2 by A8, GLIB_000:59;
e in the_Edges_of G2 by A10, GLIB_000:def 14;
then e in the_Edges_of G1 by GLIB_007:4;
then e DJoins x,v1,G1 by A1, A10, GLIB_007:7;
hence e in v1 .edgesIn() by A9, GLIB_000:57; :: thesis:

end;

assume A11: e in v1 .edgesIn() ; :: thesis:
A12: e is set by TARSKI:1;
consider x being set such that
A13: e DJoins x,v1,G1 by A11, GLIB_000:57;
e in the_Edges_of G1 by A13, GLIB_000:def 14;
then e DJoins v2,x,G2 by A1, A13, GLIB_007:7;
hence e in v2 .edgesOut() by A12, GLIB_000:59; :: thesis:

end;

hence v2 .edgesOut() = v1 .edgesIn() by TARSKI:2; :: thesis:
hence v2 .outDegree() = v1 .inDegree() ; :: thesis: