now

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

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

set X = the [Weighted] inducedSubgraph of G,V,E;
set W = (the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E);
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 2;
then dom ((the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] inducedSubgraph of G,V,E by RELAT_1:62;
then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] inducedSubgraph of G,V,E by PARTFUN1:def 2;
set GG = the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W);
A2: the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) == the [Weighted] inducedSubgraph of G,V,E by Lm3;
then the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) is Subgraph of the [Weighted] inducedSubgraph of G,V,E by GLIB_000:87;
then reconsider GG = the [Weighted] inducedSubgraph of G,V,E .set (WeightSelector,W) as Subgraph of G by GLIB_000:43;
A3: the_Vertices_of GG = the_Vertices_of the [Weighted] inducedSubgraph of G,V,E by A2, GLIB_000:def 34
.= V by A1, GLIB_000:def 37 ;
the_Edges_of GG = the_Edges_of the [Weighted] inducedSubgraph of G,V,E by A2, GLIB_000:def 34
.= E by A1, GLIB_000:def 37 ;
then reconsider GG = GG as [Weighted] inducedSubgraph of G,V,E by A1, A3, GLIB_000:def 37;
take GG = GG; :: thesis: GG is weight-inheriting
the_Weight_of GG = W by GLIB_000:8
.= (the_Weight_of G) | (the_Edges_of GG) by A2, GLIB_000:def 34 ;
hence GG is weight-inheriting by Def10; :: thesis: verum

end;

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

reconsider GG = G as Subgraph of G by GLIB_000:40;
reconsider GG = GG as [Weighted] inducedSubgraph of G,V,E by A4, GLIB_000:def 37;
take GG = GG; :: thesis: GG is weight-inheriting
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 2;
then the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) by RELAT_1:69;
hence GG is weight-inheriting by Def10; :: thesis: verum

end;

end;

end;

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