let G be loopless _Graph; :: thesis: (G .supDegree()) +` 1 c= G .tChromaticNum()
G is G .tChromaticNum() -tcolorable by Th186;
then consider t being proper TColoring of G such that
A1: card ((rng (t _V)) \/ (rng (t _E))) c= G .tChromaticNum() ;
set D = { (v .degree()) where v is Vertex of G : verum } ;

per cases ( G .supDegree() is finite or G .supDegree() is infinite ) ;

suppose G .supDegree() is finite ; :: thesis: (G .supDegree()) +` 1 c= G .tChromaticNum()

then reconsider s = G .supDegree() as Nat ;

now :: thesis: for x being object st x in (G .supDegree()) +` 1 holds
x in G .tChromaticNum()

let x be object ; :: thesis: ( x in (G .supDegree()) +` 1 implies b<sub>1</sub> in G .tChromaticNum() )
assume A2: x in (G .supDegree()) +` 1 ; :: thesis: b₁ in G .tChromaticNum()
then reconsider k = x as Ordinal ;
(G .supDegree()) +` 1 = s +` 1
.= s + 1 ;
then A3: x in s + 1 by A2;
then k in omega by ORDINAL1:10;
then reconsider k = k as Nat ;

per cases ( k = 0 or 0 < k ) ;

suppose A4: k = 0 ; :: thesis: b₁ in G .tChromaticNum()

assume not x in G .tChromaticNum() ; :: thesis: contradiction
hence contradiction by A4, ORDINAL1:16, XBOOLE_1:3; :: thesis: verum

end;

suppose 0 < k ; :: thesis: b₁ in G .tChromaticNum()

then reconsider l = k - 1 as Nat by CHORD:1;
k in Segm (s + 1) by A3;
then l + 1 < s + 1 by NAT_1:44;
then l in Segm s by XREAL_1:6, NAT_1:44;
then l in union { (v .degree()) where v is Vertex of G : verum } by GLIB_013:def 6;
then consider d being set such that
A5: ( l in d & d in { (v .degree()) where v is Vertex of G : verum } ) by TARSKI:def 4;
consider v being Vertex of G such that
A6: d = v .degree() by A5;
reconsider d = d as Cardinal by A6;
d c= s by A6, GLIB_013:35;
then reconsider d = d as Nat ;
A7: rng ((t _E) | (v .edgesInOut())) c= rng (t _E) by RELAT_1:70;
{((t _V) . v)} misses (t _E) .: (v .edgesInOut()) by Def10, ZFMISC_1:50;
then A8: {((t _V) . v)} misses rng ((t _E) | (v .edgesInOut())) by RELAT_1:115;
v in the_Vertices_of G ;
then v in dom (t _V) by PARTFUN1:def 2;
then {((t _V) . v)} c= rng (t _V) by FUNCT_1:3, ZFMISC_1:31;
then A9: {((t _V) . v)} \/ (rng ((t _E) | (v .edgesInOut()))) c= (rng (t _V)) \/ (rng (t _E)) by A7, XBOOLE_1:13;
card ({((t _V) . v)} \/ (rng ((t _E) | (v .edgesInOut())))) = (card {((t _V) . v)}) +` (card (rng ((t _E) | (v .edgesInOut())))) by A8, CARD_2:35
.= (card (rng ((t _E) | (v .edgesInOut())))) +` 1 by CARD_1:30 ;
then (card (rng ((t _E) | (v .edgesInOut())))) +` 1 c= card ((rng (t _V)) \/ (rng (t _E))) by A9, CARD_1:11;
then A10: (card (rng ((t _E) | (v .edgesInOut())))) +` 1 c= G .tChromaticNum() by A1, XBOOLE_1:1;
(t _E) | (v .edgesInOut()) is one-to-one by Def5;
then card (rng ((t _E) | (v .edgesInOut()))) = card (dom ((t _E) | (v .edgesInOut()))) by CARD_1:70
.= card ((dom (t _E)) /\ (v .edgesInOut())) by RELAT_1:61
.= card ((the_Edges_of G) /\ (v .edgesInOut())) by PARTFUN1:def 2
.= card (v .edgesInOut()) by XBOOLE_1:28
.= d by A6, GLIB_000:19 ;
then A11: d +` 1 c= G .tChromaticNum() by A10;
succ (Segm l) in succ (Segm d) by A5, ORDINAL3:3;
then Segm (l + 1) in succ (Segm d) by NAT_1:38;
then Segm (l + 1) in Segm (d + 1) by NAT_1:38;
hence x in G .tChromaticNum() by A11; :: thesis: verum

end;

end;

end;

hence (G .supDegree()) +` 1 c= G .tChromaticNum() by TARSKI:def 3; :: thesis: verum

end;

suppose A12: G .supDegree() is infinite ; :: thesis: (G .supDegree()) +` 1 c= G .tChromaticNum()

then 1 in G .supDegree() by CARD_3:85, TARSKI:def 3;
then A13: (G .supDegree()) +` 1 = G .supDegree() by A12, CARD_2:76;
A14: G .supDegree() c= G .eChromaticNum() by Th123;
G .eChromaticNum() c= G .tChromaticNum() by Th192;
hence (G .supDegree()) +` 1 c= G .tChromaticNum() by A13, A14, XBOOLE_1:1; :: thesis: verum

end;

end;