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

hereby :: thesis: ( G | _GraphSelectors in G .allComponents() implies G is connected )

assume G is connected ; :: thesis: G | _GraphSelectors in G .allComponents()
then G is Component of G by GLIB_002:30;
hence G | _GraphSelectors in G .allComponents() by Th191; :: thesis: verum

end;

assume G | _GraphSelectors in G .allComponents() ; :: thesis: G is connected
then G | _GraphSelectors is Component of G by Th189;
hence G is connected by GLIB_000:128, GLIBPRE1:38; :: thesis: verum