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