let G be _Graph; :: thesis: G .tChromaticNum() c= (G .vChromaticNum()) +` (G .eChromaticNum())

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

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

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

end;

suppose G is loopless ; :: thesis: G .tChromaticNum() c= (G .vChromaticNum()) +` (G .eChromaticNum())

then ( G is G .vChromaticNum() -vcolorable & G is G .eChromaticNum() -ecolorable ) by Th54, Th122;
hence G .tChromaticNum() c= (G .vChromaticNum()) +` (G .eChromaticNum()) by Th163, Th189; :: thesis: verum

end;

end;