let G be _Graph; :: thesis: for c being Cardinal st G is c -tcolorable holds
G .tChromaticNum() c= c
let c be Cardinal; :: thesis: ( G is c -tcolorable implies G .tChromaticNum() c= c )
assume A1: G is c -tcolorable ; :: thesis: G .tChromaticNum() c= c

per cases ( not (G .order()) +` (G .size()) in c or (G .order()) +` (G .size()) in c ) ;

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

then c c= (G .order()) +` (G .size()) by ORDINAL1:16;
then c in H₃(G) by A1;
hence G .tChromaticNum() c= c by SETFAM_1:3; :: thesis: verum

end;

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

then G .tChromaticNum() in c by Th188, ORDINAL1:12;
hence G .tChromaticNum() c= c by ORDINAL1:def 2; :: thesis: verum

end;

end;