theorem :: GLIB_003:5

for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G by Lm1;