let G be _Graph; :: thesis: for v being Vertex of G holds
( v .edgesIn() = G .edgesDBetween (the_Vertices_of G),{v} & v .edgesOut() = G .edgesDBetween {v},(the_Vertices_of G) )
let v be Vertex of G; :: thesis: ( v .edgesIn() = G .edgesDBetween (the_Vertices_of G),{v} & v .edgesOut() = G .edgesDBetween {v},(the_Vertices_of G) )

now

let e be set ; :: thesis: ( ( e in v .edgesIn() implies e in G .edgesDBetween (the_Vertices_of G),{v} ) & ( e in G .edgesDBetween (the_Vertices_of G),{v} implies e in v .edgesIn() ) )

hereby :: thesis: ( e in G .edgesDBetween (the_Vertices_of G),{v} implies e in v .edgesIn() )

assume A1: e in v .edgesIn() ; :: thesis: e in G .edgesDBetween (the_Vertices_of G),{v}
then (the_Target_of G) . e = v by Lm8;
then A2: (the_Target_of G) . e in {v} by TARSKI:def 1;
(the_Source_of G) . e in the_Vertices_of G by A1, FUNCT_2:7;
then e DSJoins the_Vertices_of G,{v},G by A1, A2, Def18;
hence e in G .edgesDBetween (the_Vertices_of G),{v} by Def33; :: thesis: verum

end;

assume A3: e in G .edgesDBetween (the_Vertices_of G),{v} ; :: thesis: e in v .edgesIn()
then e DSJoins the_Vertices_of G,{v},G by Def33;
then (the_Target_of G) . e in {v} by Def18;
then (the_Target_of G) . e = v by TARSKI:def 1;
hence e in v .edgesIn() by A3, Lm8; :: thesis: verum

end;

hence v .edgesIn() = G .edgesDBetween (the_Vertices_of G),{v} by TARSKI:2; :: thesis: v .edgesOut() = G .edgesDBetween {v},(the_Vertices_of G)

now

let e be set ; :: thesis: ( ( e in v .edgesOut() implies e in G .edgesDBetween {v},(the_Vertices_of G) ) & ( e in G .edgesDBetween {v},(the_Vertices_of G) implies e in v .edgesOut() ) )

hereby :: thesis: ( e in G .edgesDBetween {v},(the_Vertices_of G) implies e in v .edgesOut() )

assume A4: e in v .edgesOut() ; :: thesis: e in G .edgesDBetween {v},(the_Vertices_of G)
then (the_Source_of G) . e = v by Lm9;
then A5: (the_Source_of G) . e in {v} by TARSKI:def 1;
(the_Target_of G) . e in the_Vertices_of G by A4, FUNCT_2:7;
then e DSJoins {v}, the_Vertices_of G,G by A4, A5, Def18;
hence e in G .edgesDBetween {v},(the_Vertices_of G) by Def33; :: thesis: verum

end;

assume A6: e in G .edgesDBetween {v},(the_Vertices_of G) ; :: thesis: e in v .edgesOut()
then e DSJoins {v}, the_Vertices_of G,G by Def33;
then (the_Source_of G) . e in {v} by Def18;
then (the_Source_of G) . e = v by TARSKI:def 1;
hence e in v .edgesOut() by A6, Lm9; :: thesis: verum

end;

hence v .edgesOut() = G .edgesDBetween {v},(the_Vertices_of G) by TARSKI:2; :: thesis: verum