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

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