let G be _Graph; :: thesis: ( G is complete implies G is connected )
assume A1: G is complete ; :: thesis: G is connected
for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v

proof

let u, v be Vertex of G; :: thesis: ex W being Walk of G st W is_Walk_from u,v

per cases ( u = v or u <> v ) ;

suppose A2: u = v ; :: thesis: ex W being Walk of G st W is_Walk_from u,v

take G .walkOf v ; :: thesis: G .walkOf v is_Walk_from u,v
thus G .walkOf v is_Walk_from u,v by A2, GLIB_001:13; :: thesis: verum

end;

suppose u <> v ; :: thesis: ex W being Walk of G st W is_Walk_from u,v

then consider e being object such that
A3: e Joins u,v,G by A1, CHORD:def 6, CHORD:def 3;
take G .walkOf (u,e,v) ; :: thesis: G .walkOf (u,e,v) is_Walk_from u,v
thus G .walkOf (u,e,v) is_Walk_from u,v by A3, GLIB_001:15; :: thesis: verum

end;

end;

end;

hence G is connected by GLIB_002:def 1; :: thesis: verum