theorem Th1: :: GLIB_011:1

for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )