let G2 be edgeless _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .vChromaticNum() = 2
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .vChromaticNum() = 2
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .vChromaticNum() = 2
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not w in the_Vertices_of G2 implies G1 .vChromaticNum() = 2 )
assume A1: not w in the_Vertices_of G2 ; :: thesis: G1 .vChromaticNum() = 2

now :: thesis: ( G1 is 2 -vcolorable & ( for c being Cardinal st G1 is c -vcolorable holds
2 c= c ) )

thus G1 is 2 -vcolorable by Th38; :: thesis: for c being Cardinal st G1 is c -vcolorable holds
2 c= c
let c be Cardinal; :: thesis: ( G1 is c -vcolorable implies 2 c= c )
assume A2: G1 is c -vcolorable ; :: thesis: 2 c= c
assume not 2 c= c ; :: thesis: contradiction
then c in {0,1} by ORDINAL1:16, CARD_1:50;

per cases then ( c = 0 or c = 1 ) by TARSKI:def 2;

suppose c = 0 ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

suppose A3: c = 1 ; :: thesis: contradiction

not e in the_Edges_of G2 ;
then e DJoins v,w,G1 by A1, GLIB_006:131;
then e in the_Edges_of G1 by GLIB_000:def 14;
hence contradiction by A2, A3; :: thesis: verum

end;

end;

end;

hence G1 .vChromaticNum() = 2 by Th58; :: thesis: verum