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