set G2 = G .set WeightSelector ,X;
the_Weight_of (G .set WeightSelector ,X) = X by GLIB_000:11;
hence G .set WeightSelector ,X is real-weighted by Def13; :: thesis: verum