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

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