theorem :: GLIB_010:149

for G3, G4 being _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex of G4,v2
for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds
ex F being PGraphMapping of G1,G2 st
( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )