let G be _Graph; :: thesis: ( G is loopless implies G is G .tChromaticNum() -tcolorable )
assume G is loopless ; :: thesis: G is G .tChromaticNum() -tcolorable
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 A2: (G .order()) +` (G .size()) in H₃(G) by A1;

now :: thesis: for a being set st a in H₃(G) holds
a is cardinal number

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

end;

then consider c being Cardinal such that
A4: ( c in H₃(G) & c = G .tChromaticNum() ) by A2, GLIBPRE0:14;
consider c9 being cardinal Subset of ((G .order()) +` (G .size())) such that
A5: ( c = c9 & G is c9 -tcolorable ) by A4;
thus G is G .tChromaticNum() -tcolorable by A4, A5; :: thesis: verum