let v be Vertex of G; :: thesis: not v is isolated
set w = the Element of (the_Vertices_of G) \ {v};
(the_Vertices_of G) \ {v} <> {} by GLIB_000:20;
then A1: ( the Element of (the_Vertices_of G) \ {v} in the_Vertices_of G & the Element of (the_Vertices_of G) \ {v} <> v ) by ZFMISC_1:56;
then reconsider w = the Element of (the_Vertices_of G) \ {v} as Vertex of G ;
consider W being Walk of G such that
A2: W is_Walk_from v,w by GLIB_002:def 1;
w in G .reachableFrom v by A2, GLIB_002:def 5;
hence not v is isolated by A1, Th53; :: thesis: verum