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

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

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

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

end;

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

then G1 is ((G2 .tChromaticNum()) +` 1) +` (card V) -tcolorable by Th186, Th175;
hence G1 .tChromaticNum() c= ((G2 .tChromaticNum()) +` 1) +` (card V) by Th189; :: thesis: verum

end;

end;