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

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

assume x in v .inNeighbors() ; :: thesis: ex e being object st e DJoins x,v,G
then consider e being object such that
A1: e in dom (the_Source_of G) and
A2: e in v .edgesIn() and
A3: x = (the_Source_of G) . e by FUNCT_1:def 6;
take e = e; :: thesis: e DJoins x,v,G
(the_Target_of G) . e = v by A2, Lm7;
hence e DJoins x,v,G by A1, A3; :: thesis: verum

end;

given e being object such that A4: e DJoins x,v,G ; :: thesis: x in v .inNeighbors()
A5: e in the_Edges_of G by A4;
then A6: e in dom (the_Source_of G) by FUNCT_2:def 1;
(the_Target_of G) . e = v by A4;
then A7: e in v .edgesIn() by A5, Lm7;
(the_Source_of G) . e = x by A4;
hence x in v .inNeighbors() by A7, A6, FUNCT_1:def 6; :: thesis: verum