now :: thesis: ( ELabelSelector in dom (G2 .set (ELabelSelector,(the_ELabel_of G1))) & ex f being Function st

( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) ) )

hence
G2 .set (ELabelSelector,(the_ELabel_of G1)) is [ELabeled]
by GLIB_003:def 5; :: thesis: verum( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) ) )

set G3 = G2 .set (ELabelSelector,(the_ELabel_of G1));

ELabelSelector in {ELabelSelector} by TARSKI:def 1;

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

hence ELabelSelector in dom (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:7; :: thesis: ex f being Function st

( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) )

consider f being Function such that

A1: ( G1 . ELabelSelector = f & dom f c= the_Edges_of G1 ) by GLIB_003:def 5;

G2 == G2 .set (ELabelSelector,(the_ELabel_of G1)) by GLIB_003:7;

then the_Edges_of G2 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:def 34;

then A2: the_Edges_of G1 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_007:4;

take f = f; :: thesis: ( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) )

thus (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = the_ELabel_of G1 by GLIB_000:8

.= f by A1, GLIB_003:def 8 ; :: thesis: dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1)))

thus dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by A1, A2; :: thesis: verum

end;ELabelSelector in {ELabelSelector} by TARSKI:def 1;

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

hence ELabelSelector in dom (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:7; :: thesis: ex f being Function st

( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) )

consider f being Function such that

A1: ( G1 . ELabelSelector = f & dom f c= the_Edges_of G1 ) by GLIB_003:def 5;

G2 == G2 .set (ELabelSelector,(the_ELabel_of G1)) by GLIB_003:7;

then the_Edges_of G2 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:def 34;

then A2: the_Edges_of G1 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_007:4;

take f = f; :: thesis: ( (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f & dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) )

thus (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = the_ELabel_of G1 by GLIB_000:8

.= f by A1, GLIB_003:def 8 ; :: thesis: dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1)))

thus dom f c= the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by A1, A2; :: thesis: verum