set G1 = G .set (ELabelSelector,X);
( dom (G .set (ELabelSelector,X)) = (dom G) \/ {ELabelSelector} & ELabelSelector in {ELabelSelector} ) by GLIB_000:7, TARSKI:def 1;
hence ELabelSelector in dom (G .set (ELabelSelector,X)) by XBOOLE_0:def 3; :: according to GLIB_003:def 5 :: thesis: ex f being Function st
( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) )
G == G .set (ELabelSelector,X) by Lm3;
then A1: the_Edges_of G = the_Edges_of (G .set (ELabelSelector,X)) ;
dom X c= the_Edges_of G ;
hence ex f being Function st
( (G .set (ELabelSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (ELabelSelector,X)) ) by A1, GLIB_000:8; :: thesis: verum