let G1, G2 be _finite _Graph; :: thesis: 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
let F be PGraphMapping of G1,G2; :: thesis: ( F is strong_SG-embedding & ex F0 being PGraphMapping of G1,G2 st F0 is isomorphism implies F is isomorphism )
assume A1: F is strong_SG-embedding ; :: thesis: ( for F0 being PGraphMapping of G1,G2 holds not F0 is isomorphism or F is isomorphism )
given F0 being PGraphMapping of G1,G2 such that A2: F0 is isomorphism ; :: thesis: F is isomorphism
( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) by A2, Th84;
hence F is isomorphism by A1, Th51; :: thesis: verum