let V be set ; :: thesis: for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1
let G2 be _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v,V holds G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1
let G1 be addAdjVertexAll of G2,v,V; :: thesis: G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1

per cases ( not G2 is loopless or G2 is loopless ) ;

suppose not G2 is loopless ; :: thesis: G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1

then G1 .vChromaticNum() = 0 ;
hence G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1 by XBOOLE_1:2; :: thesis: verum

end;

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

then G1 is (G2 .vChromaticNum()) +` 1 -vcolorable by Th54, Th39;
hence G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1 by Th57; :: thesis: verum

end;

end;