:: deftheorem Def9 defines connected GLIB_014:def 9 :
for S being Graph-membered set holds
( S is connected iff for G being _Graph st G in S holds
G is connected );