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

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

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 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;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