let G be _Graph; :: thesis: ( G is edge-finite implies G is finite-ecolorable )
assume A1: G is edge-finite ; :: thesis: G is finite-ecolorable
G is G .size() -ecolorable by Th100;
hence G is finite-ecolorable by A1; :: thesis: verum