let G be _Graph; :: thesis: ( G is c -edge implies G is c -ecolorable )
assume A1: G is c -edge ; :: thesis: G is c -ecolorable
reconsider g = id (the_Edges_of G) as EColoring of G ;
card (rng g) = G .size()
.= c by A1, GLIB_013:def 4 ;
hence G is c -ecolorable ; :: thesis: verum