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

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

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

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

end;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() ) )

hence
G .componentSet() = {(the_Vertices_of G)}
by TARSKI:2; :: thesis: verum( ( 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() ) )

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;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 {(the_Vertices_of G)}
; :: thesis: 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;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

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

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