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