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:
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:
now :: thesis: 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 ; :: 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:
then reconsider x9 = x as Vertex of C ;
consider W being Walk of C such that
A2: W is_Walk_from v,x9 by ;
reconsider W = W as Walk of G by GLIB_001:167;
W is_Walk_from v,x by ;
hence x in G .reachableFrom v by Def5; :: thesis: verum
end;
assume A3: x in G .reachableFrom v ; :: thesis:
then reconsider x9 = x as Vertex of G ;
A4: G .reachableFrom x9 = G .reachableFrom v by ;
set CX = the inducedSubgraph of G,();
not C c< the inducedSubgraph of G,() by Def7;
then A5: ( C == the inducedSubgraph of G,() or not C c= the inducedSubgraph of G,() ) by GLIB_000:def 36;
A6: the_Edges_of the inducedSubgraph of G,() = G .edgesBetween () by GLIB_000:def 37;
now :: thesis: for e being object st e in the_Edges_of C holds
e in the_Edges_of the inducedSubgraph of G,()
let e be object ; :: thesis: ( e in the_Edges_of C implies e in the_Edges_of the inducedSubgraph of G,() )
set v1 = () . e;
set v2 = () . e;
assume A7: e in the_Edges_of C ; :: thesis: e in the_Edges_of the inducedSubgraph of G,()
then reconsider v1 = () . e, v2 = () . e as Vertex of C by FUNCT_2:5;
e Joins v1,v2,C by ;
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 ;
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 ;
reconsider W2 = W2 as Walk of G by GLIB_001:167;
W2 is_Walk_from v,v2 by ;
then A11: v2 in G .reachableFrom x9 by ;
W1 is_Walk_from v,v1 by ;
then v1 in G .reachableFrom x9 by ;
hence e in the_Edges_of the inducedSubgraph of G,() by ; :: thesis: verum
end;
then A12: the_Edges_of C c= the_Edges_of the inducedSubgraph of G,() ;
A13: the_Vertices_of the inducedSubgraph of G,() = G .reachableFrom x9 by GLIB_000:def 37;
now :: thesis: for z being object st z in the_Vertices_of C holds
z in the_Vertices_of the inducedSubgraph of G,()
let z be object ; :: thesis: ( z in the_Vertices_of C implies z in the_Vertices_of the inducedSubgraph of G,() )
assume z in the_Vertices_of C ; :: thesis: z in the_Vertices_of the inducedSubgraph of G,()
then consider W being Walk of C such that
A14: W is_Walk_from v,z by ;
reconsider W = W as Walk of G by GLIB_001:167;
W is_Walk_from v,z by ;
hence z in the_Vertices_of the inducedSubgraph of G,() by ; :: thesis: verum
end;
then the_Vertices_of C c= the_Vertices_of the inducedSubgraph of G,() ;
then A15: C is Subgraph of the inducedSubgraph of G,() by ;
x in the_Vertices_of the inducedSubgraph of G,() by ;
hence x in the_Vertices_of C by ; :: 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:
hence v in the_Vertices_of C by Lm1; :: thesis: verum