let G be _Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )

hereby :: thesis: ( the_Vertices_of C = G .reachableFrom v implies v in the_Vertices_of C )

assume A1: v in the_Vertices_of C ; :: thesis: the_Vertices_of C = G .reachableFrom v

now

let x be set ; :: thesis: ( ( x in the_Vertices_of C implies x in G .reachableFrom v ) & ( x in G .reachableFrom v implies x in the_Vertices_of C ) )

hereby :: thesis: ( x in G .reachableFrom v implies x in the_Vertices_of C )

assume x in the_Vertices_of C ; :: thesis: x in G .reachableFrom v
then reconsider x' = x as Vertex of C ;
consider W being Walk of C such that
A2: W is_Walk_from v,x' by A1, Def1;
reconsider W = W as Walk of G by GLIB_001:168;
W is_Walk_from v,x by A2, GLIB_001:20;
hence x in G .reachableFrom v by Def5; :: thesis: verum

end;

assume A3: x in G .reachableFrom v ; :: thesis: x in the_Vertices_of C
then reconsider x' = x as Vertex of G ;
consider CX being inducedSubgraph of G,(G .reachableFrom x');
( not C c< CX & not CX c< C ) by Def7;
then A4: ( ( C == CX or not C c= CX ) & ( CX == C or not CX c= C ) ) by GLIB_000:def 38;
A5: ( the_Vertices_of CX = G .reachableFrom x' & the_Edges_of CX = G .edgesBetween (G .reachableFrom x') ) by GLIB_000:def 39;
then A6: x in the_Vertices_of CX by Lm1;
A7: G .reachableFrom x' = G .reachableFrom v by A3, Lm3;

now

let z be set ; :: thesis: ( z in the_Vertices_of C implies z in the_Vertices_of CX )
assume z in the_Vertices_of C ; :: thesis: z in the_Vertices_of CX
then consider W being Walk of C such that
A8: W is_Walk_from v,z by A1, Def1;
reconsider W = W as Walk of G by GLIB_001:168;
W is_Walk_from v,z by A8, GLIB_001:20;
hence z in the_Vertices_of CX by A5, A7, Def5; :: thesis: verum

end;

then A9: the_Vertices_of C c= the_Vertices_of CX by TARSKI:def 3;

now

let e be set ; :: thesis: ( e in the_Edges_of C implies e in the_Edges_of CX )
assume A10: e in the_Edges_of C ; :: thesis: e in the_Edges_of CX
set v1 = (the_Source_of C) . e;
set v2 = (the_Target_of C) . e;
reconsider v1 = (the_Source_of C) . e, v2 = (the_Target_of C) . e as Vertex of C by A10, FUNCT_2:7;
e Joins v1,v2,C by A10, GLIB_000:def 15;
then A11: e Joins v1,v2,G by GLIB_000:75;
consider W1 being Walk of C such that
A12: W1 is_Walk_from v,v1 by A1, Def1;
reconsider W1 = W1 as Walk of G by GLIB_001:168;
A13: W1 is_Walk_from v,v1 by A12, GLIB_001:20;
consider W2 being Walk of C such that
A14: W2 is_Walk_from v,v2 by A1, Def1;
reconsider W2 = W2 as Walk of G by GLIB_001:168;
W2 is_Walk_from v,v2 by A14, GLIB_001:20;
then ( v1 in G .reachableFrom x' & v2 in G .reachableFrom x' ) by A7, A13, Def5;
hence e in the_Edges_of CX by A5, A11, GLIB_000:35; :: thesis: verum

end;

then the_Edges_of C c= the_Edges_of CX by TARSKI:def 3;
then C is Subgraph of CX by A9, GLIB_000:47;
hence x in the_Vertices_of C by A4, A6, GLIB_000:def 36, GLIB_000:def 37; :: thesis: verum

end;

hence the_Vertices_of C = G .reachableFrom v by TARSKI:2; :: thesis: verum

end;

assume the_Vertices_of C = G .reachableFrom v ; :: thesis: v in the_Vertices_of C
hence v in the_Vertices_of C by Lm1; :: thesis: verum