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 G3 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( G3 is weight-inheriting & G3 is elabel-inheriting & G3 is vlabel-inheriting )

consider X being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E;
set W = (the_Weight_of G) | (the_Edges_of X);
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 4;
then dom ((the_Weight_of G) | (the_Edges_of X)) = the_Edges_of X by RELAT_1:91;
then reconsider W = (the_Weight_of G) | (the_Edges_of X) as ManySortedSet of the_Edges_of X by PARTFUN1:def 4;
set G1 = X .set WeightSelector ,W;
set EL = (the_ELabel_of G) | (the_Edges_of (X .set WeightSelector ,W));
reconsider EL' = (the_ELabel_of G) | (the_Edges_of (X .set WeightSelector ,W)) as PartFunc of , by RELSET_1:11;
reconsider EL' = EL' as PartFunc of , by RELAT_1:87, RELSET_1:13;
set G2 = (X .set WeightSelector ,W) .set ELabelSelector ,EL';
set VL = (the_VLabel_of G) | (the_Vertices_of ((X .set WeightSelector ,W) .set ELabelSelector ,EL'));
reconsider VL' = (the_VLabel_of G) | (the_Vertices_of ((X .set WeightSelector ,W) .set ELabelSelector ,EL')) as PartFunc of , by RELSET_1:11;
reconsider VL' = VL' as PartFunc of , by RELAT_1:87, RELSET_1:13;
set G3 = ((X .set WeightSelector ,W) .set ELabelSelector ,EL') .set VLabelSelector ,VL';
A2: (X .set WeightSelector ,W) .set ELabelSelector ,EL' == X .set WeightSelector ,W by Lm3;
A3: ((X .set WeightSelector ,W) .set ELabelSelector ,EL') .set VLabelSelector ,VL' == (X .set WeightSelector ,W) .set ELabelSelector ,EL' by Lm3;
X == X .set WeightSelector ,W by Lm3;
then (X .set WeightSelector ,W) .set ELabelSelector ,EL' == X by A2, GLIB_000:88;
then A4: ((X .set WeightSelector ,W) .set ELabelSelector ,EL') .set VLabelSelector ,VL' == X by A3, GLIB_000:88;
then ((X .set WeightSelector ,W) .set ELabelSelector ,EL') .set VLabelSelector ,VL' is Subgraph of X by GLIB_000:90;
then reconsider G3 = ((X .set WeightSelector ,W) .set ELabelSelector ,EL') .set VLabelSelector ,VL' as Subgraph of G by GLIB_000:46;
A5: the_Vertices_of G3 = the_Vertices_of X by A4, GLIB_000:def 36
.= V by A1, GLIB_000:def 39 ;
the_Edges_of G3 = the_Edges_of X by A4, GLIB_000:def 36
.= E by A1, GLIB_000:def 39 ;
then reconsider G3 = G3 as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A1, A5, GLIB_000:def 39;
A6: G3 == X .set WeightSelector ,W by A2, A3, GLIB_000:88;
take G3 = G3; :: thesis: ( G3 is weight-inheriting & G3 is elabel-inheriting & G3 is vlabel-inheriting )
the_Weight_of G3 = ((X .set WeightSelector ,W) .set ELabelSelector ,EL') . WeightSelector by GLIB_000:12
.= (X .set WeightSelector ,W) . WeightSelector by GLIB_000:12
.= W by GLIB_000:11
.= (the_Weight_of G) | (the_Edges_of G3) by A4, GLIB_000:def 36 ;
hence G3 is weight-inheriting by Def10; :: thesis: ( G3 is elabel-inheriting & G3 is vlabel-inheriting )
the_ELabel_of G3 = ((X .set WeightSelector ,W) .set ELabelSelector ,EL') . ELabelSelector by GLIB_000:12
.= (the_ELabel_of G) | (the_Edges_of (X .set WeightSelector ,W)) by GLIB_000:11
.= (the_ELabel_of G) | (the_Edges_of G3) by A6, GLIB_000:def 36 ;
hence G3 is elabel-inheriting by Def11; :: thesis: G3 is vlabel-inheriting
the_VLabel_of G3 = (the_VLabel_of G) | (the_Vertices_of ((X .set WeightSelector ,W) .set ELabelSelector ,EL')) by GLIB_000:11
.= (the_VLabel_of G) | (the_Vertices_of G3) by A3, GLIB_000:def 36 ;
hence G3 is vlabel-inheriting by Def12; :: thesis: verum

end;

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

reconsider GG = G as Subgraph of G by GLIB_000:43;
reconsider GG = GG as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A7, GLIB_000:def 39;
take GG = GG; :: thesis: ( GG is weight-inheriting & GG is elabel-inheriting & GG is vlabel-inheriting )
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 4;
then the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) by RELAT_1:98;
hence GG is weight-inheriting by Def10; :: thesis: ( GG is elabel-inheriting & GG is vlabel-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: GG is vlabel-inheriting
dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
then the_VLabel_of G = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:97;
hence GG is vlabel-inheriting by Def12; :: thesis: verum

end;

end;

end;

hence ex b₁ being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b₁ is weight-inheriting & b₁ is elabel-inheriting & b₁ is vlabel-inheriting ) ; :: thesis: verum