let G2 be _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let t be TColoring of G2; :: thesis: for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let x, y be object ; :: thesis: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 implies [((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1 )
assume A1: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: [((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
then consider G3 being addVertex of G2,v such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:126;
reconsider t3 = [((t _V) +* (v .--> x)),(t _E)] as TColoring of G3 by Th140;
A3: ( v is Vertex of G3 & w is Vertex of G3 ) by GLIB_006:68, GLIB_006:94;
not e in the_Edges_of G3 by A1, GLIB_006:def 10;
then [(t3 _V),((t3 _E) +* (e .--> y))] is TColoring of G1 by A2, A3, Th141;
hence [((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1 ; :: thesis: verum