:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :
for G being GraphStruct holds
( G is [VLabeled] iff ( VLabelSelector in dom G & ex f being Function st
( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ) );