:: deftheorem Def4 defines vlabel-distinct GLIB_010:def 4 :
for G being VGraph holds
( G is vlabel-distinct iff the_VLabel_of G is one-to-one );