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