let x be object ; :: thesis: ( x in the_Vertices_of G implies b₁ in field (VertexDomRel G) )
assume x in the_Vertices_of G ; :: thesis: b₁ in field (VertexDomRel G)
then reconsider v = x as Vertex of G ;
set H = the inducedSubgraph of G,(G .reachableFrom v);
reconsider H0 = the inducedSubgraph of G,(G .reachableFrom v) as non _trivial _Graph by A1;
the_Vertices_of the inducedSubgraph of G,(G .reachableFrom v) = G .reachableFrom v by GLIB_000:def 37;
then reconsider v0 = v as Vertex of H0 by GLIB_002:9;
not (the_Vertices_of H0) \ {v0} is empty by GLIB_000:20;
then consider w being object such that
A3: w in (the_Vertices_of the inducedSubgraph of G,(G .reachableFrom v)) \ {v0} by XBOOLE_0:def 1;
reconsider w = w as Vertex of the inducedSubgraph of G,(G .reachableFrom v) by A3, XBOOLE_0:def 5;
the_Vertices_of the inducedSubgraph of G,(G .reachableFrom v) = G .reachableFrom v by GLIB_000:def 37;
then consider W being Walk of G such that
A4: W is_Walk_from v,w by GLIB_002:def 5;
A5: ( W .first() = v & W .last() = w ) by A4, GLIB_001:def 23;
not w in {v} by A3, XBOOLE_0:def 5;
then v <> w by TARSKI:def 1;
then 3 <= len W by A5, GLIB_001:125, GLIB_001:127;
then 1 < len W by XXREAL_0:2;
then W . (1 + 1) Joins W . 1,W . (1 + 2),G by GLIB_001:def 3, POLYFORM:4;
then W . 2 Joins v,W . 3,G by A5, GLIB_001:def 6;