set G2 = G .set (ELabelSelector,X);
( the_Weight_of (G .set (ELabelSelector,X)) = the_Weight_of G & rng (the_Weight_of G) c= Real>=0 ) by Def14, GLIB_000:9;
hence G .set (ELabelSelector,X) is nonnegative-weighted ; :: thesis: verum