now ex GG being [VLabeled] inducedSubgraph of G,V,E st GG 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 )
;
ex GG being [VLabeled] inducedSubgraph of G,V,E st GG is vlabel-inheriting set X = the
[VLabeled] inducedSubgraph of
G,
V,
E;
set VL =
(the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E);
reconsider VL9 =
(the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E) as
PartFunc of
(dom ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))),
(rng ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))) by RELSET_1:4;
reconsider VL9 =
VL9 as
PartFunc of
(the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E),
(rng ((the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E))) by RELAT_1:58, RELSET_1:5;
set GG = the
[VLabeled] inducedSubgraph of
G,
V,
E .set (
VLabelSelector,
VL9);
A2:
the
[VLabeled] inducedSubgraph of
G,
V,
E .set (
VLabelSelector,
VL9)
== the
[VLabeled] inducedSubgraph of
G,
V,
E
by Lm3;
then
the
[VLabeled] inducedSubgraph of
G,
V,
E .set (
VLabelSelector,
VL9) is
Subgraph of the
[VLabeled] inducedSubgraph of
G,
V,
E
by GLIB_000:87;
then reconsider GG = the
[VLabeled] inducedSubgraph of
G,
V,
E .set (
VLabelSelector,
VL9) as
Subgraph of
G by GLIB_000:43;
A3:
the_Vertices_of GG =
the_Vertices_of the
[VLabeled] inducedSubgraph of
G,
V,
E
by A2
.=
V
by A1, GLIB_000:def 37
;
the_Edges_of GG =
the_Edges_of the
[VLabeled] inducedSubgraph of
G,
V,
E
by A2
.=
E
by A1, GLIB_000:def 37
;
then reconsider GG =
GG as
[VLabeled] inducedSubgraph of
G,
V,
E by A1, A3, GLIB_000:def 37;
take GG =
GG;
GG is vlabel-inheriting the_VLabel_of GG =
(the_VLabel_of G) | (the_Vertices_of the [VLabeled] inducedSubgraph of G,V,E)
by GLIB_000:8
.=
(the_VLabel_of G) | (the_Vertices_of GG)
by A2
;
hence
GG is
vlabel-inheriting
;
verum end; end; end;
hence
ex b1 being [VLabeled] inducedSubgraph of G,V,E st b1 is vlabel-inheriting
; verum