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

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

end;

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

reconsider GG = G as Subgraph of G by GLIB_000:43;
reconsider GG = GG as [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def 39;
take GG = GG; :: 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 [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b₁ is elabel-inheriting & b₁ is vlabel-inheriting ) ; :: thesis: verum