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