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