let G be _Graph; :: thesis: G .tChromaticNum() c= (G .order()) +` (G .size())

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

suppose not G is loopless ; :: thesis: G .tChromaticNum() c= (G .order()) +` (G .size())

then G .tChromaticNum() = 0 ;
hence G .tChromaticNum() c= (G .order()) +` (G .size()) by XBOOLE_1:2; :: thesis: verum

end;

suppose G is loopless ; :: thesis: G .tChromaticNum() c= (G .order()) +` (G .size())

then ( G is G .order() -vcolorable & G is G .size() -ecolorable ) by Th29, Th100;
then A1: G is (G .order()) +` (G .size()) -tcolorable by Th163;
(G .order()) +` (G .size()) c= (G .order()) +` (G .size()) ;
then (G .order()) +` (G .size()) in H₃(G) by A1;
hence G .tChromaticNum() c= (G .order()) +` (G .size()) by SETFAM_1:3; :: thesis: verum

end;

end;