:: deftheorem Def12 defines connected GLIB_002:def 18 :
for GSq being GraphSeq holds
( GSq is connected iff for n being Nat holds GSq . n is connected );