set G0 = G .set (OrderingSelector,X);
ELabelSelector in dom G
by Def1;
then
ELabelSelector in (dom G) \/ {OrderingSelector}
by XBOOLE_0:def 3;
hence
ELabelSelector in dom (G .set (OrderingSelector,X))
by GLIB_000:7; GLIB_010:def 1 ex f being ManySortedSet of the_Edges_of (G .set (OrderingSelector,X)) st (G .set (OrderingSelector,X)) . ELabelSelector = f
consider f being ManySortedSet of the_Edges_of G such that
A1:
G . ELabelSelector = f
by Def1;
G == G .set (OrderingSelector,X)
by Th3;
then
the_Edges_of G = the_Edges_of (G .set (OrderingSelector,X))
by GLIB_000:def 34;
then reconsider f = f as ManySortedSet of the_Edges_of (G .set (OrderingSelector,X)) ;
take
f
; (G .set (OrderingSelector,X)) . ELabelSelector = f
OrderingSelector <> ELabelSelector
by GLIB_003:def 2;
hence
(G .set (OrderingSelector,X)) . ELabelSelector = f
by A1, GLIB_000:9; verum