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