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

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

assume A1: G is connected ; :: thesis: G | _GraphSelectors in G .allConnectedSG()
G is Subgraph of G by GLIB_000:40;
hence G | _GraphSelectors in G .allConnectedSG() by A1, Th125; :: thesis: verum

end;

assume G | _GraphSelectors in G .allConnectedSG() ; :: thesis: G is connected
then A2: G | _GraphSelectors is connected by Th124;
G | _GraphSelectors == G by GLIB_000:128;
hence G is connected by A2, GLIB_002:8; :: thesis: verum