let G be _Graph; :: thesis:

let V be object ; :: thesis:

hereby :: thesis:

assume V in G .componentSet() ; :: thesis:
then consider v being Vertex of G such that
A1: V = G .reachableFrom v by GLIB_002:def 8;
set C = the plain inducedSubgraph of G,(G .reachableFrom v);
reconsider C = the plain inducedSubgraph of G,(G .reachableFrom v) as _Graph ;
take C = C; :: thesis:
thus C in G .allComponents() by Th189; :: thesis:
thus V = the_Vertices_of C by A1, GLIB_000:def 37; :: thesis:

end;

given C being _Graph such that A2: ( C in G .allComponents() & V = the_Vertices_of C ) ; :: thesis:
set v = the Vertex of C;
A3: C is plain Component of G by A2, Th189;
then the_Vertices_of C c= the_Vertices_of G by GLIB_000:def 32;
then reconsider v = the Vertex of C as Vertex of G by TARSKI:def 3;
set C9 = the plain inducedSubgraph of G,(G .reachableFrom v);
A4: the_Vertices_of the plain inducedSubgraph of G,(G .reachableFrom v) = G .reachableFrom v by GLIB_000:def 37;
then the_Vertices_of the plain inducedSubgraph of G,(G .reachableFrom v) = the_Vertices_of C by A3, GLIB_002:33;
then C = the plain inducedSubgraph of G,(G .reachableFrom v) by A3, GLIB_002:32, GLIB_009:44;
hence V in G .componentSet() by A2, A4, GLIB_002:def 8; :: thesis:

end;

hence the_Vertices_of (G .allComponents()) = G .componentSet() by GLIB_014:def 14; :: thesis: