A1: dom (G .set (OrderingSelector,X)) = (dom G) \/ {OrderingSelector} by GLIB_000:7;
OrderingSelector in {OrderingSelector} by TARSKI:def 1;
then A2: OrderingSelector in dom (G .set (OrderingSelector,X)) by A1, XBOOLE_0:def 3;
not OrderingSelector in _GraphSelectors by GLIB_000:def 5, GLIB_000:1, ENUMSET1:def 2;
hence not G .set (OrderingSelector,X) is plain by A2, GLIB_009:def 1; :: thesis: verum