set G2 = G .set (OrderingSelector,X);

A1: (G .set (OrderingSelector,X)) . WeightSelector = G . WeightSelector by GLIB_003:def 1, GLIB_000:9;

WeightSelector in dom G by GLIB_003:def 4;

then WeightSelector in (dom G) \/ {OrderingSelector} by XBOOLE_0:def 3;

then A2: WeightSelector in dom (G .set (OrderingSelector,X)) by GLIB_000:7;

the_Edges_of G = the_Edges_of (G .set (OrderingSelector,X)) by Lm1, GLIB_000:10;

then (G .set (OrderingSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (OrderingSelector,X)) by A1, GLIB_003:def 4;

hence G .set (OrderingSelector,X) is [Weighted] by A2, GLIB_003:def 4; :: thesis: verum

A1: (G .set (OrderingSelector,X)) . WeightSelector = G . WeightSelector by GLIB_003:def 1, GLIB_000:9;

WeightSelector in dom G by GLIB_003:def 4;

then WeightSelector in (dom G) \/ {OrderingSelector} by XBOOLE_0:def 3;

then A2: WeightSelector in dom (G .set (OrderingSelector,X)) by GLIB_000:7;

the_Edges_of G = the_Edges_of (G .set (OrderingSelector,X)) by Lm1, GLIB_000:10;

then (G .set (OrderingSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (OrderingSelector,X)) by A1, GLIB_003:def 4;

hence G .set (OrderingSelector,X) is [Weighted] by A2, GLIB_003:def 4; :: thesis: verum