let G be _Graph; :: thesis: ( G is connected iff G .numComponents() = 1 )

then consider V being object such that

A1: G .componentSet() = {V} by CARD_2:42;

reconsider V = V as set by TARSKI:1;

V in G .componentSet() by A1, TARSKI:def 1;

then V = the_Vertices_of G by A3, XBOOLE_0:def 10;

hence G is connected by A1, Lm11; :: thesis: verum

hereby :: thesis: ( G .numComponents() = 1 implies G is connected )

assume
G .numComponents() = 1
; :: thesis: G is connected assume
G is connected
; :: thesis: G .numComponents() = 1

then G .componentSet() = {(the_Vertices_of G)} by Lm11;

hence G .numComponents() = 1 by CARD_1:30; :: thesis: verum

end;then G .componentSet() = {(the_Vertices_of G)} by Lm11;

hence G .numComponents() = 1 by CARD_1:30; :: thesis: verum

then consider V being object such that

A1: G .componentSet() = {V} by CARD_2:42;

reconsider V = V as set by TARSKI:1;

now :: thesis: for v being object st v in the_Vertices_of G holds

v in V

then A3:
the_Vertices_of G c= V
;v in V

let v be object ; :: thesis: ( v in the_Vertices_of G implies v in V )

assume v in the_Vertices_of G ; :: thesis: v in V

then reconsider v9 = v as Vertex of G ;

end;assume v in the_Vertices_of G ; :: thesis: v in V

then reconsider v9 = v as Vertex of G ;

now :: thesis: v in V

hence
v in V
; :: thesis: verumset V2 = G .reachableFrom v9;

assume A2: not v in V ; :: thesis: contradiction

G .reachableFrom v9 in G .componentSet() by Def8;

then not v in G .reachableFrom v9 by A1, A2, TARSKI:def 1;

hence contradiction by Lm1; :: thesis: verum

end;assume A2: not v in V ; :: thesis: contradiction

G .reachableFrom v9 in G .componentSet() by Def8;

then not v in G .reachableFrom v9 by A1, A2, TARSKI:def 1;

hence contradiction by Lm1; :: thesis: verum

V in G .componentSet() by A1, TARSKI:def 1;

then V = the_Vertices_of G by A3, XBOOLE_0:def 10;

hence G is connected by A1, Lm11; :: thesis: verum