for G1, G2 being _finite _Graph
for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & ex F0 being PGraphMapping of G1,G2 st F0 is isomorphism holds
F is isomorphism