:: deftheorem Def13 defines one-to-one GLIB_010:def 13 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is one-to-one iff ( F _V is one-to-one & F _E is one-to-one ) );