now :: 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 )

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

set X = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E;
set W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] [VLabeled] 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] [ELabeled] [VLabeled] inducedSubgraph of G,V,E)) = the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by RELAT_1:62;
then reconsider W = (the_Weight_of G) | (the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E) as ManySortedSet of the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by PARTFUN1:def 2;
set G1 = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W);
set EL = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)));
reconsider EL9 = (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) as PartFunc of (dom ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELSET_1:4;
reconsider EL9 = EL9 as PartFunc of (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))),(rng ((the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))))) by RELAT_1:58, RELSET_1:5;
set G2 = ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9);
set VL = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)));
reconsider VL9 = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))) as PartFunc of (dom ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))),(rng ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))) by RELSET_1:4;
reconsider VL9 = VL9 as PartFunc of (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))),(rng ((the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))))) by RELAT_1:58, RELSET_1:5;
set G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9);
A2: ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3;
A3: (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) by Lm3;
the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by Lm3;
then ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A2;
then A4: (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A3;
then (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) is Subgraph of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by GLIB_000:87;
then reconsider G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) .set (VLabelSelector,VL9) as Subgraph of G by GLIB_000:43;
A5: the_Vertices_of G3 = the_Vertices_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A4
.= V by A1, GLIB_000:def 37 ;
the_Edges_of G3 = the_Edges_of the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A4
.= E by A1, GLIB_000:def 37 ;
then reconsider G3 = G3 as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A1, A5, GLIB_000:def 37;
A6: G3 == the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W) by A2, A3;
take G3 = G3; :: thesis: ( G3 is weight-inheriting & G3 is elabel-inheriting & G3 is vlabel-inheriting )
the_Weight_of G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) . WeightSelector by GLIB_000:9
.= ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) . WeightSelector by GLIB_000:9
.= W by GLIB_000:8
.= (the_Weight_of G) | (the_Edges_of G3) by A4 ;
hence G3 is weight-inheriting ; :: thesis: ( G3 is elabel-inheriting & G3 is vlabel-inheriting )
the_ELabel_of G3 = (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9)) . ELabelSelector by GLIB_000:9
.= (the_ELabel_of G) | (the_Edges_of ( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W))) by GLIB_000:8
.= (the_ELabel_of G) | (the_Edges_of G3) by A6 ;
hence G3 is elabel-inheriting ; :: thesis: G3 is vlabel-inheriting
the_VLabel_of G3 = (the_VLabel_of G) | (the_Vertices_of (( the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E .set (WeightSelector,W)) .set (ELabelSelector,EL9))) by GLIB_000:8
.= (the_VLabel_of G) | (the_Vertices_of G3) by A3 ;
hence G3 is vlabel-inheriting ; :: thesis: verum

end;

suppose A7: ( not V is non empty Subset of (the_Vertices_of G) 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:40;
reconsider GG = GG as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A7, GLIB_000:def 37;
take GG = GG; :: thesis: ( GG is weight-inheriting & GG is elabel-inheriting & GG is vlabel-inheriting )
thus GG is weight-inheriting ; :: 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:68;
hence GG is elabel-inheriting ; :: 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:68;
hence GG is vlabel-inheriting ; :: 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