let G be _Graph; :: thesis: ( G is _trivial implies G is connected )
assume G is _trivial ; :: thesis: G is connected
then consider x being Vertex of G such that
A1: the_Vertices_of G = {x} by GLIB_000:22;

now :: thesis: for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v

set W = G .walkOf x;
let u, v be Vertex of G; :: thesis: ex W being Walk of G st W is_Walk_from u,v
( u = x & v = x ) by A1, TARSKI:def 1;
then G .walkOf x is_Walk_from u,v by GLIB_001:13;
hence ex W being Walk of G st W is_Walk_from u,v ; :: thesis: verum

end;

hence G is connected ; :: thesis: verum