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