let G be _Graph; ( ( for C being Component of G holds not C is _trivial ) implies field (VertexDomRel G) = the_Vertices_of G )
assume A1:
for C being Component of G holds not C is _trivial
; field (VertexDomRel G) = the_Vertices_of G
A2:
field (VertexDomRel G) c= (the_Vertices_of G) \/ (the_Vertices_of G)
by RELSET_1:8;
now for x being object st x in the_Vertices_of G holds
x in field (VertexDomRel G)let x be
object ;
( x in the_Vertices_of G implies b1 in field (VertexDomRel G) )assume
x in the_Vertices_of G
;
b1 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;
end;
then
the_Vertices_of G c= field (VertexDomRel G)
by TARSKI:def 3;
hence
field (VertexDomRel G) = the_Vertices_of G
by A2, XBOOLE_0:def 10; verum