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;
now :: thesis: ex u being Vertex of G st u <> v
per cases ( v1 = v or v1 <> v ) ;
suppose v1 = v ; :: thesis: ex u being Vertex of G st u <> v
hence ex u being Vertex of G st u <> v by A1; :: thesis: verum
end;
suppose v1 <> v ; :: thesis: ex u being Vertex of G st u <> v
hence ex u being Vertex of G st u <> v ; :: thesis: verum
end;
end;
end;
then consider u being Vertex of G such that
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