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