set G0 = G .set (ELabelSelector,(id (the_Edges_of G)));

ELabelSelector in {ELabelSelector} by TARSKI:def 1;

then ELabelSelector in (dom G) \/ {ELabelSelector} by XBOOLE_0:def 3;

hence ELabelSelector in dom (G .set (ELabelSelector,(id (the_Edges_of G)))) by GLIB_000:7; :: according to GLIB_010:def 1 :: thesis: ( ex f being ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) st (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f & G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct )

thus ex f being ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) st (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f :: thesis: G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct

hence G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct by GLIB_003:def 8; :: thesis: verum

ELabelSelector in {ELabelSelector} by TARSKI:def 1;

then ELabelSelector in (dom G) \/ {ELabelSelector} by XBOOLE_0:def 3;

hence ELabelSelector in dom (G .set (ELabelSelector,(id (the_Edges_of G)))) by GLIB_000:7; :: according to GLIB_010:def 1 :: thesis: ( ex f being ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) st (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f & G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct )

thus ex f being ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) st (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f :: thesis: G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct

proof

(G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = id (the_Edges_of G)
by GLIB_000:8;
G == G .set (ELabelSelector,(id (the_Edges_of G)))
by GLIB_003:7;

then the_Edges_of G = the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) by GLIB_000:def 34;

then reconsider f = id (the_Edges_of G) as ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) ;

take f ; :: thesis: (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f

thus (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f by GLIB_000:8; :: thesis: verum

end;then the_Edges_of G = the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) by GLIB_000:def 34;

then reconsider f = id (the_Edges_of G) as ManySortedSet of the_Edges_of (G .set (ELabelSelector,(id (the_Edges_of G)))) ;

take f ; :: thesis: (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f

thus (G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = f by GLIB_000:8; :: thesis: verum

hence G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct by GLIB_003:def 8; :: thesis: verum