let c be Cardinal; :: thesis: for G2 being non edgeless _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let G2 be non edgeless _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & G2 is c -tcolorable implies G1 is c +` 1 -tcolorable )
assume A1: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: ( not G2 is c -tcolorable or G1 is c +` 1 -tcolorable )
assume G2 is c -tcolorable ; :: thesis: G1 is c +` 1 -tcolorable
then consider t2 being TColoring of G2 such that
A2: ( t2 is proper & card ((rng (t2 _V)) \/ (rng (t2 _E))) c= c ) ;
set V = rng (t2 _V);
set E = rng (t2 _E);
set x = the Element of (rng (t2 _V)) \ {((t2 _V) . w)};
set y = (rng (t2 _V)) \/ (rng (t2 _E));
(rng (t2 _V)) \ {((t2 _V) . w)} <> {}

proof

assume (rng (t2 _V)) \ {((t2 _V) . w)} = {} ; :: thesis: contradiction
then ( rng (t2 _V) = {} or rng (t2 _V) = {((t2 _V) . w)} ) by ZFMISC_1:58;
then ( card (rng (t2 _V)) = 0 or card (rng (t2 _V)) = 1 ) by CARD_1:30;
then ( G2 is 0 -vcolorable or G2 is 1 -vcolorable ) by A2;
hence contradiction ; :: thesis: verum

end;

then A3: ( the Element of (rng (t2 _V)) \ {((t2 _V) . w)} in rng (t2 _V) & the Element of (rng (t2 _V)) \ {((t2 _V) . w)} <> (t2 _V) . w ) by ZFMISC_1:56;
set f = (t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)});
set g = (t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E))));
reconsider t1 = [((t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)})),((t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E)))))] as TColoring of G1 by A1, Th143;
the Element of (rng (t2 _V)) \ {((t2 _V) . w)} in (rng (t2 _V)) \/ (rng (t2 _E)) by A3, XBOOLE_0:def 3;
then ( the Element of (rng (t2 _V)) \ {((t2 _V) . w)} <> (rng (t2 _V)) \/ (rng (t2 _E)) & not (rng (t2 _V)) \/ (rng (t2 _E)) in (rng (t2 _V)) \/ (rng (t2 _E)) & t1 _V = (t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}) & t1 _E = (t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E)))) ) ;
then A4: t1 is proper by A1, A2, A3, Th158;
rng (e .--> ((rng (t2 _V)) \/ (rng (t2 _E)))) = rng {[e,((rng (t2 _V)) \/ (rng (t2 _E)))]} by FUNCT_4:82
.= {((rng (t2 _V)) \/ (rng (t2 _E)))} by RELAT_1:9 ;
then A5: rng ((t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E))))) c= (rng (t2 _E)) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))} by FUNCT_4:17;
(t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}) = (t2 _V) +* ({v} --> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}) by FUNCOP_1:def 9;
then rng ((t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)})) c= rng (t2 _V) by A3, Lm3;
then (rng ((t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}))) \/ (rng ((t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E)))))) c= (rng (t2 _V)) \/ ((rng (t2 _E)) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))}) by A5, XBOOLE_1:13;
then (rng ((t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}))) \/ (rng ((t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E)))))) c= ((rng (t2 _V)) \/ (rng (t2 _E))) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))} by XBOOLE_1:4;
then A6: card ((rng ((t2 _V) +* (v .--> the Element of (rng (t2 _V)) \ {((t2 _V) . w)}))) \/ (rng ((t2 _E) +* (e .--> ((rng (t2 _V)) \/ (rng (t2 _E))))))) c= card (((rng (t2 _V)) \/ (rng (t2 _E))) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))}) by CARD_1:11;
not (rng (t2 _V)) \/ (rng (t2 _E)) in (rng (t2 _V)) \/ (rng (t2 _E)) ;
then card (((rng (t2 _V)) \/ (rng (t2 _E))) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))}) = (card ((rng (t2 _V)) \/ (rng (t2 _E)))) +` (card {((rng (t2 _V)) \/ (rng (t2 _E)))}) by ZFMISC_1:50, CARD_2:35
.= (card ((rng (t2 _V)) \/ (rng (t2 _E)))) +` 1 by CARD_1:30 ;
then card (((rng (t2 _V)) \/ (rng (t2 _E))) \/ {((rng (t2 _V)) \/ (rng (t2 _E)))}) c= c +` 1 by A2, CARD_2:84;
hence G1 is c +` 1 -tcolorable by A4, A6, XBOOLE_1:1; :: thesis: verum