:: deftheorem defines vlabel-preserving GLIB_010:def 27 :
for G1, G2 being VGraph
for F being PGraphMapping of G1,G2 holds
( F is vlabel-preserving iff (the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V)) );