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 ;

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

hence
G is connected
; :: thesis: verumlet 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;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