let G be _Graph; :: thesis: ( G is edgeless iff G is 0 -ecolorable )

hereby :: thesis: ( G is 0 -ecolorable implies G is edgeless )

assume G is edgeless ; :: thesis: G is 0 -ecolorable
then G .size() = 0 ;
hence G is 0 -ecolorable by Th100; :: thesis: verum

end;

assume G is 0 -ecolorable ; :: thesis: G is edgeless
then consider g being proper EColoring of G such that
A1: card (rng g) c= 0 ;
card (rng g) = 0 by A1, XBOOLE_1:3;
then g = {} ;
then {} = dom g
.= the_Edges_of G by PARTFUN1:def 2 ;
hence G is edgeless ; :: thesis: verum