let G be _Graph; :: thesis: ( G is edgeless iff G is 1 -tcolorable )

hereby :: thesis: ( G is 1 -tcolorable implies G is edgeless )

assume A1: G is edgeless ; :: thesis: G is 1 -tcolorable
then G is 1 -vcolorable ;
then consider f being VColoring of G such that
A2: ( f is proper & card (rng f) c= 1 ) ;
reconsider t = [f,{}] as TColoring of G by A1, Th137;
A3: t is proper by A2;
card ((rng (t _V)) \/ (rng (t _E))) = card ((rng (t _V)) \/ (rng {}))
.= card (rng (t _V)) ;
hence G is 1 -tcolorable by A2, A3; :: thesis: verum

end;

assume G is 1 -tcolorable ; :: thesis: G is edgeless
then G is 1 -vcolorable by Th162;
hence G is edgeless ; :: thesis: verum