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
proof
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;
(G .set (ELabelSelector,(id (the_Edges_of G)))) . ELabelSelector = id (the_Edges_of G) by GLIB_000:8;
hence G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct by GLIB_003:def 8; :: thesis: verum