A3:
dom (G .set (VLabelSelector,X)) = (dom G) \/ {VLabelSelector}
by GLIB_000:7;

VLabelSelector in {VLabelSelector} by TARSKI:def 1;

then VLabelSelector in dom (G .set (VLabelSelector,X)) by A3, XBOOLE_0:def 3;

hence not G .set (VLabelSelector,X) is plain by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 3, ENUMSET1:def 2; :: thesis: verum

VLabelSelector in {VLabelSelector} by TARSKI:def 1;

then VLabelSelector in dom (G .set (VLabelSelector,X)) by A3, XBOOLE_0:def 3;

hence not G .set (VLabelSelector,X) is plain by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 3, ENUMSET1:def 2; :: thesis: verum