:: deftheorem Def1 defines connected GLIB_002:def 1 :
for G being _Graph holds
( G is connected iff for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v );