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

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

VLabelSelector in dom G by GLIB_003:def 6;

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

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

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

then ex f being Function st

( (G .set (OrderingSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (OrderingSelector,X)) ) by A1, GLIB_003:def 6;

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

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

VLabelSelector in dom G by GLIB_003:def 6;

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

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

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

then ex f being Function st

( (G .set (OrderingSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (OrderingSelector,X)) ) by A1, GLIB_003:def 6;

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