let G be _Graph; :: thesis: ( G is connected iff G .componentSet() = {(the_Vertices_of G)} )

hereby :: thesis: ( G .componentSet() = {(the_Vertices_of G)} implies G is connected )

assume A1: G is connected ; :: thesis: G .componentSet() = {(the_Vertices_of G)}

now :: thesis: for x being object holds
( ( x in G .componentSet() implies x in {(the_Vertices_of G)} ) & ( x in {(the_Vertices_of G)} implies x in G .componentSet() ) )

set v = the Vertex of G;
let x be object ; :: thesis: ( ( x in G .componentSet() implies x in {(the_Vertices_of G)} ) & ( x in {(the_Vertices_of G)} implies x in G .componentSet() ) )

hereby :: thesis: ( x in {(the_Vertices_of G)} implies x in G .componentSet() )

assume x in G .componentSet() ; :: thesis: x in {(the_Vertices_of G)}
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: verum

end;

assume x in {(the_Vertices_of G)} ; :: thesis: x in G .componentSet()
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: verum

end;

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

end;

assume G .componentSet() = {(the_Vertices_of G)} ; :: thesis: G is connected
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: verum