theorem :: GLIB_002:30

for G being _Graph holds
( G is Component of G iff G is connected )