:: deftheorem Def10 defines PVM2PGM GLIB_011:def 10 :
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2
for b₄ being PGraphMapping of G1,G2 holds
( b₄ = PVM2PGM f iff ( b₄ _V = f & dom (b₄ _E) = G1 .edgesBetween (dom f) & rng (b₄ _E) c= G2 .edgesBetween (rng f) ) );