let G be loopless non edgeless _Graph; :: thesis: 3 c= G .tChromaticNum()
assume not 3 c= G .tChromaticNum() ; :: thesis: contradiction
then G .tChromaticNum() in 3 by ORDINAL1:16;

per cases then ( G .tChromaticNum() = 0 or G .tChromaticNum() = 1 or G .tChromaticNum() = 2 ) by CARD_1:51, ENUMSET1:def 1;

suppose G .tChromaticNum() = 0 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose G .tChromaticNum() = 1 ; :: thesis: contradiction

hence contradiction by Th195; :: thesis: verum

end;

suppose G .tChromaticNum() = 2 ; :: thesis: contradiction

then G is 2 -tcolorable by Th186;
then consider t being TColoring of G such that
A1: ( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= 2 ) ;
2 c= card ((rng (t _V)) \/ (rng (t _E)))

proof

assume not 2 c= card ((rng (t _V)) \/ (rng (t _E))) ; :: thesis: contradiction
then card ((rng (t _V)) \/ (rng (t _E))) in 2 by ORDINAL1:16;

per cases then ( card ((rng (t _V)) \/ (rng (t _E))) = 0 or card ((rng (t _V)) \/ (rng (t _E))) = 1 ) by CARD_1:50, TARSKI:def 2;

suppose card ((rng (t _V)) \/ (rng (t _E))) = 0 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose card ((rng (t _V)) \/ (rng (t _E))) = 1 ; :: thesis: contradiction

then G is 1 -tcolorable by A1;
hence contradiction ; :: thesis: verum

end;

end;

end;

then consider a, b being object such that
A2: ( a <> b & (rng (t _V)) \/ (rng (t _E)) = {a,b} ) by A1, XBOOLE_0:def 10, CARD_2:60;
set e = the Element of the_Edges_of G;
set v = (the_Source_of G) . the Element of the_Edges_of G;
set w = (the_Target_of G) . the Element of the_Edges_of G;
( the Element of the_Edges_of G Joins (the_Source_of G) . the Element of the_Edges_of G,(the_Target_of G) . the Element of the_Edges_of G,G & the Element of the_Edges_of G Joins (the_Target_of G) . the Element of the_Edges_of G,(the_Source_of G) . the Element of the_Edges_of G,G ) by GLIB_000:def 13;
then A3: ( (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) <> (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) & (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) <> (t _E) . the Element of the_Edges_of G & (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) <> (t _E) . the Element of the_Edges_of G ) by A1, Th148;
the Element of the_Edges_of G in the_Edges_of G ;
then the Element of the_Edges_of G in dom (t _E) by PARTFUN1:def 2;
then (t _E) . the Element of the_Edges_of G in rng (t _E) by FUNCT_1:3;
then (t _E) . the Element of the_Edges_of G in {a,b} by A2, XBOOLE_0:def 3;
then A4: ( (t _E) . the Element of the_Edges_of G = a or (t _E) . the Element of the_Edges_of G = b ) by TARSKI:def 2;
( (the_Source_of G) . the Element of the_Edges_of G in the_Vertices_of G & (the_Target_of G) . the Element of the_Edges_of G in the_Vertices_of G ) ;
then ( (the_Source_of G) . the Element of the_Edges_of G in dom (t _V) & (the_Target_of G) . the Element of the_Edges_of G in dom (t _V) ) by PARTFUN1:def 2;
then ( (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) in rng (t _V) & (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) in rng (t _V) ) by FUNCT_1:3;
then ( (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) in {a,b} & (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) in {a,b} ) by A2, XBOOLE_0:def 3;
then ( ( (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) = a or (t _V) . ((the_Source_of G) . the Element of the_Edges_of G) = b ) & ( (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) = a or (t _V) . ((the_Target_of G) . the Element of the_Edges_of G) = b ) ) by TARSKI:def 2;
hence contradiction by A3, A4; :: thesis: verum

end;

end;