now ex b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )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] )set X = the
inducedSubgraph of
G,
V,
E;
set W = the
ManySortedSet of
the_Edges_of the
inducedSubgraph of
G,
V,
E;
set G2 = the
inducedSubgraph of
G,
V,
E .set (
WeightSelector, the
ManySortedSet of
the_Edges_of the
inducedSubgraph of
G,
V,
E);
set EL = the
PartFunc of
(the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),
REAL;
set G3 =
( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),
REAL);
set VL = the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL;
set G4 =
(( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL);
( the
inducedSubgraph of
G,
V,
E == the
inducedSubgraph of
G,
V,
E .set (
WeightSelector, the
ManySortedSet of
the_Edges_of the
inducedSubgraph of
G,
V,
E) & the
inducedSubgraph of
G,
V,
E .set (
WeightSelector, the
ManySortedSet of
the_Edges_of the
inducedSubgraph of
G,
V,
E)
== ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),
REAL) )
by Lm3;
then A2:
the
inducedSubgraph of
G,
V,
E == ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),
REAL)
;
( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),
REAL)
== (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL)
by Lm3;
then A3:
the
inducedSubgraph of
G,
V,
E == (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL)
by A2;
then
(( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL) is
Subgraph of the
inducedSubgraph of
G,
V,
E
by GLIB_000:87;
then reconsider G4 =
(( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of (( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E)) .set (ELabelSelector, the PartFunc of (the_Edges_of ( the inducedSubgraph of G,V,E .set (WeightSelector, the ManySortedSet of the_Edges_of the inducedSubgraph of G,V,E))),REAL))),
REAL) as
Subgraph of
G by GLIB_000:43;
the_Edges_of the
inducedSubgraph of
G,
V,
E = E
by A1, GLIB_000:def 37;
then A4:
the_Edges_of G4 = E
by A3;
the_Vertices_of the
inducedSubgraph of
G,
V,
E = V
by A1, GLIB_000:def 37;
then
the_Vertices_of G4 = V
by A3;
then
G4 is
inducedSubgraph of
G,
V,
E
by A1, A4, GLIB_000:def 37;
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] )set W = the
ManySortedSet of
the_Edges_of G;
set G2 =
G .set (
WeightSelector, the
ManySortedSet of
the_Edges_of G);
set EL = the
PartFunc of
(the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),
REAL;
set G3 =
(G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),
REAL);
set VL = the
PartFunc of
(the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),
REAL;
set G4 =
((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),
REAL);
(
G == G .set (
WeightSelector, the
ManySortedSet of
the_Edges_of G) &
G .set (
WeightSelector, the
ManySortedSet of
the_Edges_of G)
== (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),
REAL) )
by Lm3;
then A6:
G == (G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),
REAL)
;
(G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (
ELabelSelector, the
PartFunc of
(the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),
REAL)
== ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),
REAL)
by Lm3;
then A7:
G == ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),
REAL)
by A6;
then reconsider G4 =
((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL)) .set (
VLabelSelector, the
PartFunc of
(the_Vertices_of ((G .set (WeightSelector, the ManySortedSet of the_Edges_of G)) .set (ELabelSelector, the PartFunc of (the_Edges_of (G .set (WeightSelector, the ManySortedSet of the_Edges_of G))),REAL))),
REAL) as
Subgraph of
G by GLIB_000:87;
G4 is
inducedSubgraph of
G,
V,
E
by A5, A7, GLIB_000:def 37;
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