let G be _Graph; :: thesis: ( G is edgeless iff G .tChromaticNum() = 1 )

hereby :: thesis: ( G .tChromaticNum() = 1 implies G is edgeless )

assume A1: G is edgeless ; :: thesis: G .tChromaticNum() = 1

now :: thesis: for c being Cardinal st G is c -tcolorable holds
1 c= c

let c be Cardinal; :: thesis: ( G is c -tcolorable implies 1 c= c )
assume A2: G is c -tcolorable ; :: thesis: 1 c= c
assume not 1 c= c ; :: thesis: contradiction
then c in 1 by ORDINAL1:16;
then c = 0 by CARD_1:49, TARSKI:def 1;
hence contradiction by A2; :: thesis: verum

end;

hence G .tChromaticNum() = 1 by A1, Th190; :: thesis: verum

end;

assume G .tChromaticNum() = 1 ; :: thesis: G is edgeless
then G is 1 -tcolorable by Th186, Th187;
hence G is edgeless ; :: thesis: verum