for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng (F | H) st F9 = F | H holds
( ( F is weak_SG-embedding implies F9 is weak_SG-embedding ) & ( F is strong_SG-embedding implies F9 is isomorphism ) & ( F is directed & F is strong_SG-embedding implies F9 is Disomorphism ) )