let G be _Graph; :: thesis: for e being set
for v being Vertex of G holds
( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )
let e be set ; :: thesis: for v being Vertex of G holds
( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )
let v be Vertex of G; :: thesis: ( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )

hereby :: thesis: ( ex x being set st e DJoins v,x,G implies e in v .edgesOut() )

set x = (the_Target_of G) . e;
assume A1: e in v .edgesOut() ; :: thesis: ex x being set st e DJoins v,x,G
take x = (the_Target_of G) . e; :: thesis: e DJoins v,x,G
(the_Source_of G) . e = v by A1, Lm8;
hence e DJoins v,x,G by A1; :: thesis: verum

end;

given x being set such that A2: e DJoins v,x,G ; :: thesis: e in v .edgesOut()
( e in the_Edges_of G & (the_Source_of G) . e = v ) by A2;
hence e in v .edgesOut() by Lm8; :: thesis: verum