let G2 be _Graph; :: thesis: for c being Cardinal
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let c be Cardinal; :: thesis: for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let e be object ; :: thesis: for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let v, w be Vertex of G2; :: thesis: for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let G1 be addEdge of G2,v,e,w; :: thesis: ( v,w are_adjacent & G2 is c -tcolorable implies G1 is c +` 1 -tcolorable )
assume A1: ( v,w are_adjacent & G2 is c -tcolorable ) ; :: thesis: G1 is c +` 1 -tcolorable

per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;

suppose A2: not e in the_Edges_of G2 ; :: thesis: G1 is c +` 1 -tcolorable

consider t being TColoring of G2 such that
A3: ( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c ) by A1;
set V = rng (t _V);
set E = rng (t _E);
set y = (rng (t _V)) \/ (rng (t _E));
set g = (t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E))));
reconsider t1 = [(t _V),((t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E)))))] as TColoring of G1 by A2, Th141;
( not (rng (t _V)) \/ (rng (t _E)) in (rng (t _V)) \/ (rng (t _E)) & t1 _V = t _V & t1 _E = (t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E)))) ) ;
then A4: t1 is proper by A1, A2, A3, Th155;
rng (e .--> ((rng (t _V)) \/ (rng (t _E)))) = rng {[e,((rng (t _V)) \/ (rng (t _E)))]} by FUNCT_4:82
.= {((rng (t _V)) \/ (rng (t _E)))} by RELAT_1:9 ;
then (rng (t _V)) \/ (rng ((t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E)))))) c= (rng (t _V)) \/ ((rng (t _E)) \/ {((rng (t _V)) \/ (rng (t _E)))}) by FUNCT_4:17, XBOOLE_1:9;
then (rng (t _V)) \/ (rng ((t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E)))))) c= ((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E)))} by XBOOLE_1:4;
then A5: card ((rng (t _V)) \/ (rng ((t _E) +* (e .--> ((rng (t _V)) \/ (rng (t _E))))))) c= card (((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E)))}) by CARD_1:11;
not (rng (t _V)) \/ (rng (t _E)) in (rng (t _V)) \/ (rng (t _E)) ;
then card (((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E)))}) = (card ((rng (t _V)) \/ (rng (t _E)))) +` (card {((rng (t _V)) \/ (rng (t _E)))}) by ZFMISC_1:50, CARD_2:35
.= (card ((rng (t _V)) \/ (rng (t _E)))) +` 1 by CARD_1:30 ;
then card (((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E)))}) c= c +` 1 by A3, CARD_2:84;
hence G1 is c +` 1 -tcolorable by A4, A5, XBOOLE_1:1; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: G1 is c +` 1 -tcolorable

then G1 == G2 by GLIB_006:def 11;
then G1 is c -tcolorable by A1, Th167;
hence G1 is c +` 1 -tcolorable by Th161, CARD_2:94; :: thesis: verum

end;

end;