let G be _Graph; :: thesis: ( G is edgeless iff G .eChromaticNum() = 0 )

hereby :: thesis: ( G .eChromaticNum() = 0 implies G is edgeless )

assume G is edgeless ; :: thesis: G .eChromaticNum() = 0
then G .size() = 0 ;
hence G .eChromaticNum() = 0 by Th120, XBOOLE_1:3; :: thesis: verum

end;

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