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

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

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 .set (VLabelSelector,(id (the_Vertices_of G)))) . VLabelSelector = id (the_Vertices_of G)
by GLIB_000:8;
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;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

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