set G0 = G .set (VLabelSelector,(id (the_Vertices_of G)));
VLabelSelector in {VLabelSelector} by TARSKI:def 1;
then VLabelSelector in (dom G) \/ {VLabelSelector} by XBOOLE_0:def 3;
hence VLabelSelector in dom (G .set (VLabelSelector,(id (the_Vertices_of G)))) by GLIB_000:7; :: according to GLIB_010:def 2 :: thesis: ( ex f being ManySortedSet of the_Vertices_of (G .set (VLabelSelector,(id (the_Vertices_of G)))) st (G .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = f & G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct )
thus ex f being ManySortedSet of the_Vertices_of (G .set (VLabelSelector,(id (the_Vertices_of G)))) st (G .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = f :: thesis: G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct

proof

G == G .set (VLabelSelector,(id (the_Vertices_of G))) by GLIB_003:7;
then the_Vertices_of G = the_Vertices_of (G .set (VLabelSelector,(id (the_Vertices_of G)))) by GLIB_000:def 34;
then reconsider f = id (the_Vertices_of G) as ManySortedSet of the_Vertices_of (G .set (VLabelSelector,(id (the_Vertices_of G)))) ;
take f ; :: thesis: (G .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = f
thus (G .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = f by GLIB_000:8; :: thesis: verum

end;

(G .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = id (the_Vertices_of G) by GLIB_000:8;
hence G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct by GLIB_003:def 9; :: thesis: verum