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 :: thesis: for e being object holds
( ( 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() ) )

let e be object ; :: 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 Lm7;
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:5;
then e DSJoins the_Vertices_of G,{v},G by A1, A2;
hence e in G .edgesDBetween ((the_Vertices_of G),{v}) by Def31; :: 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 Def31;
then (the_Target_of G) . e = v by TARSKI:def 1;
hence e in v .edgesIn() by A3, Lm7; :: 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 :: thesis: for e being object holds
( ( 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() ) )

let e be object ; :: 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 Lm8;
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:5;
then e DSJoins {v}, the_Vertices_of G,G by A4, A5;
hence e in G .edgesDBetween ({v},(the_Vertices_of G)) by Def31; :: 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 Def31;
then (the_Source_of G) . e = v by TARSKI:def 1;
hence e in v .edgesOut() by A6, Lm8; :: thesis: verum

end;

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