set W = the ManySortedSet of the_Edges_of G;
set G2 = G .set (WeightSelector, the ManySortedSet of the_Edges_of G);
set E = 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 V = 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 A1: 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 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 A1;
then ((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) is Subgraph of G by GLIB_000:87;
hence ex b₁ being Subgraph of G st
( b₁ is [Weighted] & b₁ is [ELabeled] & b₁ is [VLabeled] ) ; :: thesis: verum