set G2 = G .set (OrderingSelector,X);
A1: (G .set (OrderingSelector,X)) . ELabelSelector = G . ELabelSelector by GLIB_003:def 2, GLIB_000:9;
ELabelSelector in dom G by GLIB_003:def 5;
then ELabelSelector in (dom G) \/ {OrderingSelector} by XBOOLE_0:def 3;
then A2: ELabelSelector 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 ex f being Function st
( (G .set (OrderingSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (OrderingSelector,X)) ) by A1, GLIB_003:def 5;
hence G .set (OrderingSelector,X) is [ELabeled] by A2, GLIB_003:def 5; :: thesis: verum