set G1 = G .set WeightSelector ,X;
( dom (G .set WeightSelector ,X) = (dom G) \/ {WeightSelector } & WeightSelector in {WeightSelector } ) by GLIB_000:9, TARSKI:def 1;
hence WeightSelector in dom (G .set WeightSelector ,X) by XBOOLE_0:def 3; :: according to GLIB_003:def 4 :: thesis: (G .set WeightSelector ,X) . WeightSelector is ManySortedSet of the_Edges_of (G .set WeightSelector ,X)
G == G .set WeightSelector ,X by Lm3;
then the_Edges_of G = the_Edges_of (G .set WeightSelector ,X) by GLIB_000:def 36;
hence (G .set WeightSelector ,X) . WeightSelector is ManySortedSet of the_Edges_of (G .set WeightSelector ,X) by GLIB_000:11; :: thesis: verum