now

per cases ( ( V is non empty Subset of & E c= G .edgesBetween V ) or not V is non empty Subset of or not E c= G .edgesBetween V ) ;

suppose A1: ( V is non empty Subset of & E c= G .edgesBetween V ) ; :: thesis: ex GG being [ELabeled] inducedSubgraph of G,V,E st GG is elabel-inheriting

consider X being [ELabeled] inducedSubgraph of G,V,E;
set EL = (the_ELabel_of G) | (the_Edges_of X);
reconsider EL' = (the_ELabel_of G) | (the_Edges_of X) as PartFunc of , by RELSET_1:11;
reconsider EL' = EL' as PartFunc of , by RELAT_1:87, RELSET_1:13;
set GG = X .set ELabelSelector ,EL';
A2: X .set ELabelSelector ,EL' == X by Lm3;
then X .set ELabelSelector ,EL' is Subgraph of X by GLIB_000:90;
then reconsider GG = X .set ELabelSelector ,EL' as Subgraph of G by GLIB_000:46;
A3: the_Vertices_of GG = the_Vertices_of X by A2, GLIB_000:def 36
.= V by A1, GLIB_000:def 39 ;
the_Edges_of GG = the_Edges_of X by A2, GLIB_000:def 36
.= E by A1, GLIB_000:def 39 ;
then reconsider GG = GG as [ELabeled] inducedSubgraph of G,V,E by A1, A3, GLIB_000:def 39;
take GG = GG; :: thesis: GG is elabel-inheriting
the_ELabel_of GG = (the_ELabel_of G) | (the_Edges_of X) by GLIB_000:11
.= (the_ELabel_of G) | (the_Edges_of GG) by A2, GLIB_000:def 36 ;
hence GG is elabel-inheriting by Def11; :: thesis: verum

end;

suppose A4: ( not V is non empty Subset of or not E c= G .edgesBetween V ) ; :: thesis: ex GG being [ELabeled] inducedSubgraph of G,V,E st GG is elabel-inheriting

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

end;

end;

end;

hence ex b₁ being [ELabeled] inducedSubgraph of G,V,E st b₁ is elabel-inheriting ; :: thesis: verum