let G be VGraph; :: thesis: dom (the_VLabel_of G) c= the_Vertices_of G
ex f being Function st
( G . VLabelSelector = f & dom f c= the_Vertices_of G ) by Def6;
hence dom (the_VLabel_of G) c= the_Vertices_of G ; :: thesis: verum