let G be _Graph; :: thesis: for c being Cardinal st G is c -tcolorable & ( for d being Cardinal st G is d -tcolorable holds
c c= d ) holds
G .tChromaticNum() = c
let c be Cardinal; :: thesis: ( G is c -tcolorable & ( for d being Cardinal st G is d -tcolorable holds
c c= d ) implies G .tChromaticNum() = c )
assume G is c -tcolorable ; :: thesis: ( ex d being Cardinal st
( G is d -tcolorable & not c c= d ) or G .tChromaticNum() = c )
then A1: ( G .tChromaticNum() c= c & G is loopless ) by Th189;
assume A2: for d being Cardinal st G is d -tcolorable holds
c c= d ; :: thesis: G .tChromaticNum() = c
( G is G .order() -vcolorable & G is G .size() -ecolorable ) by A1, Th29, Th100;
then A3: G is (G .order()) +` (G .size()) -tcolorable by Th163;
(G .order()) +` (G .size()) c= (G .order()) +` (G .size()) ;
then A4: (G .order()) +` (G .size()) in H₃(G) by A3;

now :: thesis: for x being set st x in H₃(G) holds
c c= x

let x be set ; :: thesis: ( x in H₃(G) implies c c= x )
assume x in H₃(G) ; :: thesis: c c= x
then consider d being cardinal Subset of ((G .order()) +` (G .size())) such that
A5: ( x = d & G is d -tcolorable ) ;
thus c c= x by A2, A5; :: thesis: verum

end;

then c c= G .tChromaticNum() by A4, SETFAM_1:5;
hence G .tChromaticNum() = c by A1, XBOOLE_0:def 10; :: thesis: verum