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

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

for e1, e2, v1, v2 being object

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

let G1 be addAdjVertex of G3,v1,e1,v3; :: thesis: for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

let G2 be addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

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

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

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

then consider F being PGraphMapping of G1,G2 such that

A1: F = [((F0 _V) +* (v1 .--> v2)),((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 ) and

A5: ( F0 is directed implies F is directed ) by Th155;

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

thus F = [((F0 _V) +* (v1 .--> v2)),((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 ) & ( F0 is Disomorphism implies F is Disomorphism ) )

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

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

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

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

for e1, e2, v1, v2 being object

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

let G1 be addAdjVertex of G3,v1,e1,v3; :: thesis: for G2 being addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

let G2 be addAdjVertex 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 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

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

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

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

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

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

then consider F being PGraphMapping of G1,G2 such that

A1: F = [((F0 _V) +* (v1 .--> v2)),((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 ) and

A5: ( F0 is directed implies F is directed ) by Th155;

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

thus F = [((F0 _V) +* (v1 .--> v2)),((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 ) & ( F0 is Disomorphism implies F is Disomorphism ) )

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

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

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