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

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

assume e in v .edgesIn() ; :: thesis: ex x being set st e DJoins x,v,G
then A1: ( e in the_Edges_of G & (the_Target_of G) . e = v ) by Lm8;
set x = (the_Source_of G) . e;
take x = (the_Source_of G) . e; :: thesis: e DJoins x,v,G
thus e DJoins x,v,G by A1, Def16; :: thesis: verum

end;

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