let G be _Graph; :: thesis: ( 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 implies G is connected )
given v1 being Vertex of G such that A1: for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 ; :: thesis: G is connected

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 v1,x by A1;
consider W2 being Walk of G such that
A3: W2 is_Walk_from v1,y by A1;
W1 .reverse() is_Walk_from x,v1 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