set G2 = G .set (WeightSelector,X);
the_ELabel_of (G .set (WeightSelector,X)) = the_ELabel_of G by GLIB_000:9;
hence G .set (WeightSelector,X) is real-elabeled ; :: thesis: verum