let V be set ; :: thesis: for G2 being _Graph
for G1 being addVertices of G2,V holds G1 .tChromaticNum() = G2 .tChromaticNum()
let G2 be _Graph; :: thesis: for G1 being addVertices of G2,V holds G1 .tChromaticNum() = G2 .tChromaticNum()
let G1 be addVertices of G2,V; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

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

suppose not G2 is loopless ; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

then ( G1 .tChromaticNum() = 0 & G2 .tChromaticNum() = 0 ) ;
hence G1 .tChromaticNum() = G2 .tChromaticNum() ; :: thesis: verum

end;

suppose G2 is loopless ; :: thesis: G1 .tChromaticNum() = G2 .tChromaticNum()

then ( G1 is G2 .tChromaticNum() -tcolorable & ( for c being Cardinal st G1 is c -tcolorable holds
G2 .tChromaticNum() c= c ) ) by Th169, Th186, Th189;
hence G1 .tChromaticNum() = G2 .tChromaticNum() by Th190; :: thesis: verum

end;

end;