for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st ( for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) ) holds
F _V is PVertexMapping of G1,G2