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