:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :
for G being VGraph
for G2 being [VLabeled] Subgraph of G holds
( G2 is vlabel-inheriting iff the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) );