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:12;
hence G .set ELabelSelector ,X is nonnegative-weighted by Def14; :: thesis: verum