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() )

set x = (the_Source_of G) . e;
assume A1: e in v .edgesIn() ; :: thesis: ex x being set st e DJoins x,v,G
take x = (the_Source_of G) . e; :: thesis: e DJoins x,v,G
(the_Target_of G) . e = v by A1, Lm7;
hence e DJoins x,v,G by A1; :: 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;
hence e in v .edgesIn() by Lm7; :: thesis: verum