let G be _Graph; :: thesis:

hereby :: thesis:

assume A1: G is connected ; :: thesis:

now :: thesis:

set v = the Vertex of G;
let x be object ; :: thesis:

hereby :: thesis:

assume x in G .componentSet() ; :: thesis:
then ex v being Vertex of G st x = G .reachableFrom v by Def8;
then x = the_Vertices_of G by A1, Lm8;
hence x in {(the_Vertices_of G)} by TARSKI:def 1; :: thesis:

end;

assume x in {(the_Vertices_of G)} ; :: thesis:
then A2: x = the_Vertices_of G by TARSKI:def 1;
G .reachableFrom the Vertex of G = the_Vertices_of G by A1, Lm8;
hence x in G .componentSet() by A2, Def8; :: thesis:

end;

hence G .componentSet() = {(the_Vertices_of G)} by TARSKI:2; :: thesis:

end;

assume G .componentSet() = {(the_Vertices_of G)} ; :: thesis:
then the_Vertices_of G in G .componentSet() by TARSKI:def 1;
then ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G by Def8;
hence G is connected by Lm7; :: thesis: