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; GLIB_010:def 6 (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; verum