set G1 = G .set VLabelSelector ,X;
A4: dom G c= dom (G .set VLabelSelector ,X) by FUNCT_4:11;
ELabelSelector in dom G by Def5;
hence ELabelSelector in dom (G .set VLabelSelector ,X) by A4; :: according to GLIB_003:def 5 :: thesis: ex f being Function st
( (G .set VLabelSelector ,X) . ELabelSelector = f & dom f c= the_Edges_of (G .set VLabelSelector ,X) )
G == G .set VLabelSelector ,X by Lm3;
then A5: the_Edges_of G = the_Edges_of (G .set VLabelSelector ,X) by GLIB_000:def 36;
A6: (G .set VLabelSelector ,X) . ELabelSelector = the_ELabel_of G by GLIB_000:12;
dom (the_ELabel_of G) c= the_Edges_of G by Lm1;
hence ex f being Function st
( (G .set VLabelSelector ,X) . ELabelSelector = f & dom f c= the_Edges_of (G .set VLabelSelector ,X) ) by A5, A6; :: thesis: verum