reconsider GG = G as [VLabeled] Subgraph of G by GLIB_000:40;
take GG ; :: thesis: GG is vlabel-inheriting
dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:68;
hence GG is vlabel-inheriting ; :: thesis: verum