theorem :: GLIB_002:6

for G being _Graph st ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 holds
G is connected by Lm6;