set G0 = G .set (VLabelSelector,X);
G . ELabelSelector = (G .set (VLabelSelector,X)) . ELabelSelector by GLIB_000:9, GLIB_003:def 2, GLIB_003:def 3;
then the_ELabel_of G = (G .set (VLabelSelector,X)) . ELabelSelector by GLIB_003:def 8;
hence G .set (VLabelSelector,X) is elabel-distinct by GLIB_003:def 8; :: thesis: verum