reconsider GG = G as [ELabeled] Subgraph of G by GLIB_000:43;
take GG ; :: thesis: GG is elabel-inheriting
dom (the_ELabel_of G) c= the_Edges_of G by Lm1;
then the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of G) by RELAT_1:97;
hence GG is elabel-inheriting by Def11; :: thesis: verum