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 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 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 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 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 ) )

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