theorem :: GLCOLO00:47

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )