:: deftheorem defines .labeledV() GLIB_003:def 23 :
for G being VGraph holds G .labeledV() = dom (the_VLabel_of G);