let G3, G4 be _Graph; :: thesis: for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let v1, v3 be Vertex of G3; :: thesis: for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let v2, v4 be Vertex of G4; :: thesis: for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let e1, e2 be object ; :: thesis: for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G1 be addEdge of G3,v1,e1,v3; :: thesis: for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G2 be addEdge of G4,v2,e2,v4; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) implies ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) )

assume ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

then consider F being PGraphMapping of G1,G2 such that

A1: F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is one-to-one implies F is one-to-one ) by Th152;

take F ; :: thesis: ( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3, A4; :: thesis: verum

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let v1, v3 be Vertex of G3; :: thesis: for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let v2, v4 be Vertex of G4; :: thesis: for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let e1, e2 be object ; :: thesis: for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G1 be addEdge of G3,v1,e1,v3; :: thesis: for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let G2 be addEdge of G4,v2,e2,v4; :: thesis: for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

let F0 be PGraphMapping of G3,G4; :: thesis: ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) implies ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) )

assume ( not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) ) ; :: thesis: ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

then consider F being PGraphMapping of G1,G2 such that

A1: F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] and

A2: ( F0 is total implies F is total ) and

A3: ( F0 is onto implies F is onto ) and

A4: ( F0 is one-to-one implies F is one-to-one ) by Th152;

take F ; :: thesis: ( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] by A1; :: thesis: ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

thus ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) by A2, A4; :: thesis: ( F0 is isomorphism implies F is isomorphism )

thus ( F0 is isomorphism implies F is isomorphism ) by A2, A3, A4; :: thesis: verum