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 b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )consider X being
inducedSubgraph of
G,
V,
E;
consider W being
ManySortedSet of
the_Edges_of X;
set G2 =
X .set (
WeightSelector,
W);
consider EL being
PartFunc of
(the_Edges_of (X .set (WeightSelector,W))),
REAL;
set G3 =
(X .set (WeightSelector,W)) .set (
ELabelSelector,
EL);
consider VL being
PartFunc of
(the_Vertices_of ((X .set (WeightSelector,W)) .set (ELabelSelector,EL))),
REAL;
set G4 =
((X .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL);
(
X == X .set (
WeightSelector,
W) &
X .set (
WeightSelector,
W)
== (X .set (WeightSelector,W)) .set (
ELabelSelector,
EL) )
by Lm3;
then A2:
X == (X .set (WeightSelector,W)) .set (
ELabelSelector,
EL)
by GLIB_000:88;
(X .set (WeightSelector,W)) .set (
ELabelSelector,
EL)
== ((X .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL)
by Lm3;
then A3:
X == ((X .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL)
by A2, GLIB_000:88;
then
((X .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL) is
Subgraph of
X
by GLIB_000:90;
then reconsider G4 =
((X .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL) as
Subgraph of
G by GLIB_000:46;
the_Edges_of X = E
by A1, GLIB_000:def 39;
then A4:
the_Edges_of G4 = E
by A3, GLIB_000:def 36;
the_Vertices_of X = V
by A1, GLIB_000:def 39;
then
the_Vertices_of G4 = V
by A3, GLIB_000:def 36;
then
G4 is
inducedSubgraph of
G,
V,
E
by A1, A4, GLIB_000:def 39;
hence
ex
b1 being
inducedSubgraph of
G,
V,
E st
(
b1 is
[Weighted] &
b1 is
[ELabeled] &
b1 is
[VLabeled] )
;
verum end; suppose A5:
( not
V is non
empty Subset of
(the_Vertices_of G) or not
E c= G .edgesBetween V )
;
ex b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )consider W being
ManySortedSet of
the_Edges_of G;
set G2 =
G .set (
WeightSelector,
W);
consider EL being
PartFunc of
(the_Edges_of (G .set (WeightSelector,W))),
REAL;
set G3 =
(G .set (WeightSelector,W)) .set (
ELabelSelector,
EL);
consider VL being
PartFunc of
(the_Vertices_of ((G .set (WeightSelector,W)) .set (ELabelSelector,EL))),
REAL;
set G4 =
((G .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL);
(
G == G .set (
WeightSelector,
W) &
G .set (
WeightSelector,
W)
== (G .set (WeightSelector,W)) .set (
ELabelSelector,
EL) )
by Lm3;
then A6:
G == (G .set (WeightSelector,W)) .set (
ELabelSelector,
EL)
by GLIB_000:88;
(G .set (WeightSelector,W)) .set (
ELabelSelector,
EL)
== ((G .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL)
by Lm3;
then A7:
G == ((G .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL)
by A6, GLIB_000:88;
then reconsider G4 =
((G .set (WeightSelector,W)) .set (ELabelSelector,EL)) .set (
VLabelSelector,
VL) as
Subgraph of
G by GLIB_000:90;
G4 is
inducedSubgraph of
G,
V,
E
by A5, A7, GLIB_000:def 39;
hence
ex
b1 being
inducedSubgraph of
G,
V,
E st
(
b1 is
[Weighted] &
b1 is
[ELabeled] &
b1 is
[VLabeled] )
;
verum end;
hence
ex b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
; verum