:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :
for G being EGraph
for G2 being [ELabeled] Subgraph of G holds
( G2 is elabel-inheriting iff the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) );