theorem :: GLIB_002:25

for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} ) by Lm11;