reconsider g = id (the_Edges_of G) as EColoring of G ;
take g ; :: thesis: ( g is one-to-one & g is proper )
thus ( g is one-to-one & g is proper ) ; :: thesis: verum