set G3 = G2 .set (VLabelSelector,(the_VLabel_of G1));
the_VLabel_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) = (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector by GLIB_003:def 9
.= the_VLabel_of G1 by GLIB_000:8 ;
hence G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-distinct ; :: thesis: verum