let G be EGraph; :: thesis: dom (the_ELabel_of G) c= the_Edges_of G
consider f being Function such that
A1: ( G . ELabelSelector = f & dom f c= the_Edges_of G ) by Def5;
thus dom (the_ELabel_of G) c= the_Edges_of G by A1; :: thesis: verum