set G3 = G2 .set (ELabelSelector,(the_ELabel_of G1));
the_ELabel_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) = (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector by GLIB_003:def 8
.= the_ELabel_of G1 by GLIB_000:8 ;
hence G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-distinct ; :: thesis: verum