consider W being ManySortedSet of the_Edges_of G;
set G2 = G .set (WeightSelector,W);
consider E being PartFunc of (the_Edges_of (G .set (WeightSelector,W))),REAL;
set G3 = (G .set (WeightSelector,W)) .set (ELabelSelector,E);
consider V being PartFunc of (the_Vertices_of ((G .set (WeightSelector,W)) .set (ELabelSelector,E))),REAL;
set G4 = ((G .set (WeightSelector,W)) .set (ELabelSelector,E)) .set (VLabelSelector,V);
( G == G .set (WeightSelector,W) & G .set (WeightSelector,W) == (G .set (WeightSelector,W)) .set (ELabelSelector,E) ) by Lm3;
then A1: G == (G .set (WeightSelector,W)) .set (ELabelSelector,E) by GLIB_000:88;
(G .set (WeightSelector,W)) .set (ELabelSelector,E) == ((G .set (WeightSelector,W)) .set (ELabelSelector,E)) .set (VLabelSelector,V) by Lm3;
then G == ((G .set (WeightSelector,W)) .set (ELabelSelector,E)) .set (VLabelSelector,V) by A1, GLIB_000:88;
then ((G .set (WeightSelector,W)) .set (ELabelSelector,E)) .set (VLabelSelector,V) is Subgraph of G by GLIB_000:90;
hence ex b₁ being Subgraph of G st
( b₁ is [Weighted] & b₁ is [ELabeled] & b₁ is [VLabeled] ) ; :: thesis: verum