:: deftheorem Def10 defines empty GLIB_010:def 10 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is empty iff dom (F _V) is empty );