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 )
;
ex GG being [Weighted] inducedSubgraph of G,V,E st GG is weight-inheriting consider X being
[Weighted] 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 GG =
X .set WeightSelector ,
W;
A2:
X .set WeightSelector ,
W == X
by Lm3;
then
X .set WeightSelector ,
W is
Subgraph of
X
by GLIB_000:90;
then reconsider GG =
X .set WeightSelector ,
W 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
[Weighted] inducedSubgraph of
G,
V,
E by A1, A3, GLIB_000:def 39;
take GG =
GG;
GG is weight-inheriting the_Weight_of GG =
W
by GLIB_000:11
.=
(the_Weight_of G) | (the_Edges_of GG)
by A2, GLIB_000:def 36
;
hence
GG is
weight-inheriting
by Def10;
verum end;
hence
ex b1 being [Weighted] inducedSubgraph of G,V,E st b1 is weight-inheriting
; verum