set G2 = G .set VLabelSelector ,X;
the_ELabel_of (G .set VLabelSelector ,X) = the_ELabel_of G by GLIB_000:12;
hence G .set VLabelSelector ,X is real-elabeled by Def15; :: thesis: verum