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