for G3, G4 being _Graph
for v1, v3 being Vertex of G3
for v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3
for G2 being addEdge of G4,v2,e2,v4
for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds
ex F being PGraphMapping of G1,G2 st
( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )