set G2 = G .set (ELabelSelector,X);
the_Weight_of (G .set (ELabelSelector,X)) = the_Weight_of G by GLIB_000:9;
hence G .set (ELabelSelector,X) is real-weighted ; :: thesis: verum