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

OrderingSelector in {OrderingSelector} by TARSKI:def 1;

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

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

not OrderingSelector in _GraphSelectors by GLIB_000:1, GLIB_000:def 5, ENUMSET1:def 2;

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

thus (G .set (OrderingSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (OrderingSelector,X))) by A1, GLIB_000:8; :: thesis: verum

OrderingSelector in {OrderingSelector} by TARSKI:def 1;

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

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

not OrderingSelector in _GraphSelectors by GLIB_000:1, GLIB_000:def 5, ENUMSET1:def 2;

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

thus (G .set (OrderingSelector,X)) . OrderingSelector is Enumeration of (the_Vertices_of (G .set (OrderingSelector,X))) by A1, GLIB_000:8; :: thesis: verum