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