let G be _Graph; :: thesis: G is G .size() -ecolorable
reconsider g = id (the_Edges_of G) as proper EColoring of G ;
card (rng g) = G .size() ;
hence G is G .size() -ecolorable ; :: thesis: verum