theorem :: GLIB_002:16

for G being _Graph st G is connected holds
for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G by Lm8;