theorem :: GLIB_002:28
for G being _Graph holds
( G is connected iff G .numComponents() = 1 ) by Lm18;