:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :
for G being GraphStruct holds
( G is [ELabeled] iff ( ELabelSelector in dom G & ex f being Function st
( G . ELabelSelector = f & dom f c= the_Edges_of G ) ) );