let G be _Graph; :: thesis: ( G is connected iff G .numComponents() = 1 )
hereby :: thesis: ( G .numComponents() = 1 implies 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;
assume G .numComponents() = 1 ; :: thesis: G is connected
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
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 ;
now :: thesis: v in V
set 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;
hence v in V ; :: thesis: verum
end;
then A3: the_Vertices_of G c= V ;
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