theorem :: GLIB_002:9

for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v by Lm1;