theorem Th115: :: GLCOLO00:115

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )