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;

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

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