theorem :: GLIB_000:56

for G being _Graph
for e being set
for v being Vertex of G holds
( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) by Lm7;