set G2 = G .set (VLabelSelector,X);
the_VLabel_of (G .set (VLabelSelector,X)) = X by GLIB_000:8;
hence G .set (VLabelSelector,X) is real-vlabeled by Def16; :: thesis: verum