theorem :: GLIB_002:15

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