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

per cases ( ( v is Vertex of G2 & w is Vertex of G2 & not e in the_Edges_of G2 ) or not v is Vertex of G2 or not w is Vertex of G2 or e in the_Edges_of G2 ) ;

suppose A2: ( v is Vertex of G2 & w is Vertex of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 is c +` 2 -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 x = (rng (t _V)) \/ (rng (t _E));
set y = {((rng (t _V)) \/ (rng (t _E)))};
set f = (t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E))));
set g = (t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))});
reconsider t1 = [((t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E))))),((t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))}))] as TColoring of G1 by A2, Th142;
A4: ( {((rng (t _V)) \/ (rng (t _E))),{((rng (t _V)) \/ (rng (t _E)))}} misses (rng (t _V)) \/ (rng (t _E)) & (rng (t _V)) \/ (rng (t _E)) <> {((rng (t _V)) \/ (rng (t _E)))} )

proof

A5: not (rng (t _V)) \/ (rng (t _E)) in (rng (t _V)) \/ (rng (t _E)) ;
not {((rng (t _V)) \/ (rng (t _E)))} in (rng (t _V)) \/ (rng (t _E)) by TARSKI:def 1;
hence {((rng (t _V)) \/ (rng (t _E))),{((rng (t _V)) \/ (rng (t _E)))}} misses (rng (t _V)) \/ (rng (t _E)) by A5, ZFMISC_1:51; :: thesis: (rng (t _V)) \/ (rng (t _E)) <> {((rng (t _V)) \/ (rng (t _E)))}
(rng (t _V)) \/ (rng (t _E)) in {((rng (t _V)) \/ (rng (t _E)))} by TARSKI:def 1;
hence (rng (t _V)) \/ (rng (t _E)) <> {((rng (t _V)) \/ (rng (t _E)))} ; :: thesis: verum

end;

( t1 _V = (t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E)))) & t1 _E = (t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))}) ) ;
then A6: t1 is proper by A1, A2, A3, A4, Th156;
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 A7: rng ((t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))})) c= (rng (t _E)) \/ {{((rng (t _V)) \/ (rng (t _E)))}} by FUNCT_4:17;
rng (v .--> ((rng (t _V)) \/ (rng (t _E)))) = rng {[v,((rng (t _V)) \/ (rng (t _E)))]} by FUNCT_4:82
.= {((rng (t _V)) \/ (rng (t _E)))} by RELAT_1:9 ;
then rng ((t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E))))) c= (rng (t _V)) \/ {((rng (t _V)) \/ (rng (t _E)))} by FUNCT_4:17;
then A8: (rng ((t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E)))))) \/ (rng ((t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))}))) c= ((rng (t _V)) \/ {((rng (t _V)) \/ (rng (t _E)))}) \/ ((rng (t _E)) \/ {{((rng (t _V)) \/ (rng (t _E)))}}) by A7, XBOOLE_1:13;
A9: ((rng (t _V)) \/ {((rng (t _V)) \/ (rng (t _E)))}) \/ ((rng (t _E)) \/ {{((rng (t _V)) \/ (rng (t _E)))}}) = (rng (t _V)) \/ ({((rng (t _V)) \/ (rng (t _E)))} \/ ((rng (t _E)) \/ {{((rng (t _V)) \/ (rng (t _E)))}})) by XBOOLE_1:4
.= (rng (t _V)) \/ (({((rng (t _V)) \/ (rng (t _E)))} \/ {{((rng (t _V)) \/ (rng (t _E)))}}) \/ (rng (t _E))) by XBOOLE_1:4
.= ((rng (t _V)) \/ (rng (t _E))) \/ ({((rng (t _V)) \/ (rng (t _E)))} \/ {{((rng (t _V)) \/ (rng (t _E)))}}) by XBOOLE_1:4
.= ((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E))),{((rng (t _V)) \/ (rng (t _E)))}} by ENUMSET1:1 ;
card (((rng (t _V)) \/ (rng (t _E))) \/ {((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))),{((rng (t _V)) \/ (rng (t _E)))}}) by A4, CARD_2:35
.= (card ((rng (t _V)) \/ (rng (t _E)))) +` 2 by A4, CARD_2:57 ;
then A10: card (((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E))),{((rng (t _V)) \/ (rng (t _E)))}}) c= c +` 2 by A3, CARD_2:84;
card ((rng ((t _V) +* (v .--> ((rng (t _V)) \/ (rng (t _E)))))) \/ (rng ((t _E) +* (e .--> {((rng (t _V)) \/ (rng (t _E)))})))) c= card (((rng (t _V)) \/ (rng (t _E))) \/ {((rng (t _V)) \/ (rng (t _E))),{((rng (t _V)) \/ (rng (t _E)))}}) by A8, A9, CARD_1:11;
hence G1 is c +` 2 -tcolorable by A6, A10, XBOOLE_1:1; :: thesis: verum

end;

suppose ( not v is Vertex of G2 or not w is Vertex of G2 or e in the_Edges_of G2 ) ; :: thesis: G1 is c +` 2 -tcolorable

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

end;

end;