theorem :: GLIB_002:11
for G being _Graph
for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)