let G be _Graph; :: thesis: ( ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G implies G is connected )
assume ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G ; :: thesis: G is connected
then consider v being Vertex of G such that
A1: G .reachableFrom v = the_Vertices_of G ;

now :: thesis: for x, y being Vertex of G ex W being Walk of G st W is_Walk_from x,y

let x, y be Vertex of G; :: thesis: ex W being Walk of G st W is_Walk_from x,y
consider W1 being Walk of G such that
A2: W1 is_Walk_from v,x by A1, Def5;
consider W2 being Walk of G such that
A3: W2 is_Walk_from v,y by A1, Def5;
W1 .reverse() is_Walk_from x,v by A2, GLIB_001:23;
then (W1 .reverse()) .append W2 is_Walk_from x,y by A3, GLIB_001:31;
hence ex W being Walk of G st W is_Walk_from x,y ; :: thesis: verum

end;

hence G is connected ; :: thesis: verum