:: deftheorem Def2 defines vlabel-full GLIB_010:def 2 :
for G being _Graph holds
( G is vlabel-full iff ( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f ) );