let G be _Graph; :: thesis: ( G is connected iff G .allComponents() = {(G | _GraphSelectors)} )

hereby :: thesis: ( G .allComponents() = {(G | _GraphSelectors)} implies G is connected )

assume A1: G is connected ; :: thesis: G .allComponents() = {(G | _GraphSelectors)}
then A2: {(G | _GraphSelectors)} c= G .allComponents() by Th192, ZFMISC_1:31;

now :: thesis: for x being object st x in G .allComponents() holds
x in {(G | _GraphSelectors)}

let x be object ; :: thesis: ( x in G .allComponents() implies x in {(G | _GraphSelectors)} )
assume x in G .allComponents() ; :: thesis: x in {(G | _GraphSelectors)}
then reconsider H = x as plain Component of G by Th189;
A3: G == H by A1, GLIB_006:55;
G == G | _GraphSelectors by GLIB_000:128;
then H = G | _GraphSelectors by A3, GLIB_000:85, GLIB_009:44;
hence x in {(G | _GraphSelectors)} by TARSKI:def 1; :: thesis: verum

end;

then G .allComponents() c= {(G | _GraphSelectors)} by TARSKI:def 3;
hence G .allComponents() = {(G | _GraphSelectors)} by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume {(G | _GraphSelectors)} = G .allComponents() ; :: thesis: G is connected
then G | _GraphSelectors in G .allComponents() by TARSKI:def 1;
hence G is connected by Th192; :: thesis: verum