theorem :: GLIB_002:7

for G being _trivial _Graph holds G is connected ;