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