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

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