let G be EGraph; :: thesis: dom (the_ELabel_of G) c= the_Edges_of G
ex f being Function st
( G . ELabelSelector = f & dom f c= the_Edges_of G ) by Def5;
hence dom (the_ELabel_of G) c= the_Edges_of G ; :: thesis: verum