let G2 be _Graph; :: thesis: for v being Vertex of G2
for e, w being object
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 w in the_Vertices_of G2 holds
[((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let v be Vertex of G2; :: thesis: for e, w being object
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 w in the_Vertices_of G2 holds
[((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let e, w be object ; :: 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 w in the_Vertices_of G2 holds
[((t _V) +* (w .--> 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 w in the_Vertices_of G2 holds
[((t _V) +* (w .--> 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 w in the_Vertices_of G2 holds
[((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
let x, y be object ; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 implies [((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1 )
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis: [((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1
then consider G3 being addVertex of G2,w such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:125;
reconsider t3 = [((t _V) +* (w .--> 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) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1 ; :: thesis: verum