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