theorem :: GLIB_003:6

for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;