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