let G2 be non edgeless _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 .tChromaticNum() c= (G2 .tChromaticNum()) +` 1
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds G1 .tChromaticNum() c= (G2 .tChromaticNum()) +` 1
let G1 be addAdjVertex of G2,v,e,w; :: thesis: G1 .tChromaticNum() c= (G2 .tChromaticNum()) +` 1

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

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

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

end;

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

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

end;

end;