let G be non trivial connected _Graph; :: thesis: for v being Vertex of G holds not v is isolated

let v be Vertex of G; :: thesis: not v is isolated

consider v1, v2 being Vertex of G such that

A1: v1 <> v2 by GLIB_000:21;

A2: u <> v ;

consider W being Walk of G such that

A3: W is_Walk_from u,v by Def1;

A4: W .first() = u by A3, GLIB_001:def 23;

A5: W .last() = v by A3, GLIB_001:def 23;

then v in W .vertices() by GLIB_001:88;

hence not v is isolated by A2, A4, A5, GLIB_001:127, GLIB_001:135; :: thesis: verum

let v be Vertex of G; :: thesis: not v is isolated

consider v1, v2 being Vertex of G such that

A1: v1 <> v2 by GLIB_000:21;

now :: thesis: ex u being Vertex of G st u <> v

then consider u being Vertex of G such that end;

A2: u <> v ;

consider W being Walk of G such that

A3: W is_Walk_from u,v by Def1;

A4: W .first() = u by A3, GLIB_001:def 23;

A5: W .last() = v by A3, GLIB_001:def 23;

then v in W .vertices() by GLIB_001:88;

hence not v is isolated by A2, A4, A5, GLIB_001:127, GLIB_001:135; :: thesis: verum