theorem :: GLIB_000:58

for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) by Lm8;