now 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 )
;
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;
( 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
;
( 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
;
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
;
verum end; end; end;
hence
ex b1 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting )
; verum