set G1 = G .set (VLabelSelector,X);

OrderingSelector in dom G by Def6;

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

hence OrderingSelector in dom (G .set (VLabelSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 6 :: thesis: (G .set (VLabelSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (VLabelSelector,X)))

G == G .set (VLabelSelector,X) by GLIB_003:7;

then A3: the_Vertices_of G = the_Vertices_of (G .set (VLabelSelector,X)) by GLIB_000:def 34;

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

hence (G .set (VLabelSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (VLabelSelector,X))) by A3, Def6; :: thesis: verum

OrderingSelector in dom G by Def6;

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

hence OrderingSelector in dom (G .set (VLabelSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 6 :: thesis: (G .set (VLabelSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (VLabelSelector,X)))

G == G .set (VLabelSelector,X) by GLIB_003:7;

then A3: the_Vertices_of G = the_Vertices_of (G .set (VLabelSelector,X)) by GLIB_000:def 34;

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

hence (G .set (VLabelSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (VLabelSelector,X))) by A3, Def6; :: thesis: verum