let G be _Graph; ( 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
; G is connected
then consider v being Vertex of G such that
A1:
G .reachableFrom v = the_Vertices_of G
;
now for x, y being Vertex of G ex W being Walk of G st W is_Walk_from x,ylet x,
y be
Vertex of
G;
ex W being Walk of G st W is_Walk_from x,yconsider 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
;
verum end;
hence
G is connected
; verum