theorem Th117: :: GLCOLO00:117

for G2 being _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )