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

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

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

end;

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