let G be _Graph; for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
let C be Component of G; for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
let v be Vertex of G; ( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
hereby ( the_Vertices_of C = G .reachableFrom v implies v in the_Vertices_of C )
assume A1:
v in the_Vertices_of C
;
the_Vertices_of C = G .reachableFrom vnow for x being object holds
( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )let x be
object ;
( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )assume A3:
x in G .reachableFrom v
;
x in the_Vertices_of Cthen reconsider x9 =
x as
Vertex of
G ;
A4:
G .reachableFrom x9 = G .reachableFrom v
by A3, Lm3;
set CX = the
inducedSubgraph of
G,
(G .reachableFrom x9);
not
C c< the
inducedSubgraph of
G,
(G .reachableFrom x9)
by Def7;
then A5:
(
C == the
inducedSubgraph of
G,
(G .reachableFrom x9) or not
C c= the
inducedSubgraph of
G,
(G .reachableFrom x9) )
by GLIB_000:def 36;
A6:
the_Edges_of the
inducedSubgraph of
G,
(G .reachableFrom x9) = G .edgesBetween (G .reachableFrom x9)
by GLIB_000:def 37;
now for e being object st e in the_Edges_of C holds
e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)let e be
object ;
( e in the_Edges_of C implies e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9) )set v1 =
(the_Source_of C) . e;
set v2 =
(the_Target_of C) . e;
assume A7:
e in the_Edges_of C
;
e in the_Edges_of the inducedSubgraph of G,(G .reachableFrom x9)then reconsider v1 =
(the_Source_of C) . e,
v2 =
(the_Target_of C) . e as
Vertex of
C by FUNCT_2:5;
e Joins v1,
v2,
C
by A7, GLIB_000:def 13;
then A8:
e Joins v1,
v2,
G
by GLIB_000:72;
consider W1 being
Walk of
C such that A9:
W1 is_Walk_from v,
v1
by A1, Def1;
reconsider W1 =
W1 as
Walk of
G by GLIB_001:167;
consider W2 being
Walk of
C such that A10:
W2 is_Walk_from v,
v2
by A1, Def1;
reconsider W2 =
W2 as
Walk of
G by GLIB_001:167;
W2 is_Walk_from v,
v2
by A10, GLIB_001:19;
then A11:
v2 in G .reachableFrom x9
by A4, Def5;
W1 is_Walk_from v,
v1
by A9, GLIB_001:19;
then
v1 in G .reachableFrom x9
by A4, Def5;
hence
e in the_Edges_of the
inducedSubgraph of
G,
(G .reachableFrom x9)
by A6, A8, A11, GLIB_000:32;
verum end; then A12:
the_Edges_of C c= the_Edges_of the
inducedSubgraph of
G,
(G .reachableFrom x9)
;
A13:
the_Vertices_of the
inducedSubgraph of
G,
(G .reachableFrom x9) = G .reachableFrom x9
by GLIB_000:def 37;
then
the_Vertices_of C c= the_Vertices_of the
inducedSubgraph of
G,
(G .reachableFrom x9)
;
then A15:
C is
Subgraph of the
inducedSubgraph of
G,
(G .reachableFrom x9)
by A12, GLIB_000:44;
x in the_Vertices_of the
inducedSubgraph of
G,
(G .reachableFrom x9)
by A13, Lm1;
hence
x in the_Vertices_of C
by A5, A15, GLIB_000:def 34, GLIB_000:def 35;
verum end; hence
the_Vertices_of C = G .reachableFrom v
by TARSKI:2;
verum
end;
assume
the_Vertices_of C = G .reachableFrom v
; v in the_Vertices_of C
hence
v in the_Vertices_of C
by Lm1; verum