theorem :: GLIB_000:147

for G being _Graph
for v being Vertex of G holds
( v .edgesIn() = (the_Target_of G) " {v} & v .edgesOut() = (the_Source_of G) " {v} )