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