:: deftheorem defines .inNeighbors() GLIB_000:def 46 :
for G being _Graph
for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn());