let G2 be loopless _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1
let G1 be addAdjVertexAll of G2,v; :: thesis: ( not v in the_Vertices_of G2 implies G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1 )
assume A1: not v in the_Vertices_of G2 ; :: thesis: G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1
A2: G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1 by Th70;
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: G2 .vChromaticNum() c= G1 .vChromaticNum() by Th63;

per cases ( G2 .vChromaticNum() is finite or G2 .vChromaticNum() is infinite ) ;

suppose G2 .vChromaticNum() is finite ; :: thesis: G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1

then reconsider C2 = G2 .vChromaticNum() as Nat ;
A5: G1 .vChromaticNum() c= C2 +` 1 by A2;
then reconsider C1 = G1 .vChromaticNum() as Nat ;
A6: C1 <= C2 + 1 by A5, FIELD_5:3;

now :: thesis: not C1 <> C2 + 1

assume C1 <> C2 + 1 ; :: thesis: contradiction
then C1 < C2 + 1 by A6, XXREAL_0:1;
then A7: C1 <= C2 by NAT_1:13;
C2 <= C1 by A4, FIELD_5:3;
then C1 = C2 by A7, XXREAL_0:1;
then G1 is C2 -vcolorable by Th54;
then consider f1 being VColoring of G1 such that
A8: ( f1 is proper & card (rng f1) c= C2 ) ;
reconsider R1 = rng f1 as finite set by A8;
reconsider f2 = f1 | (the_Vertices_of G2) as proper VColoring of G2 by A3, A8, Th3, Th15;
reconsider R2 = rng f2 as Subset of R1 by RELAT_1:70;
G2 is card R2 -vcolorable ;
then C2 c= card R2 by Th57;
then A9: card R1 c= card R2 by A8, XBOOLE_1:1;
card R2 c= card R1 by CARD_1:11;
then A10: R1 = R2 by A9, XBOOLE_0:def 10, CARD_2:102;
reconsider v = v as Vertex of G1 by A1, GLIB_007:50;
v in the_Vertices_of G1 ;
then v in dom f1 by PARTFUN1:def 2;
then f1 . v in R2 by A10, FUNCT_1:3;
then consider u being object such that
A11: ( u in dom f2 & f2 . u = f1 . v ) by FUNCT_1:def 3;
A12: f1 . u = f1 . v by A11, FUNCT_1:47;
A13: u in the_Vertices_of G2 by A11;
then reconsider u = u as Vertex of G1 by GLIB_006:68;
u in v .allNeighbors() by A1, A13, GLIBPRE0:55;
hence contradiction by A8, A12, GLIBPRE1:41; :: thesis: verum

end;

then C1 = C2 +` 1 ;
hence G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1 ; :: thesis: verum

end;

suppose A14: G2 .vChromaticNum() is infinite ; :: thesis: G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1

then A15: omega c= G2 .vChromaticNum() by ORDINAL1:16, CARD_1:61;
1 in omega ;
then G2 .vChromaticNum() = (G2 .vChromaticNum()) +` 1 by A14, A15, CARD_2:76;
hence G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1 by A2, A4, XBOOLE_0:def 10; :: thesis: verum

end;

end;