theorem Th109: :: GLCOLO00:109

for V being set
for c being Cardinal
for G2 being b₂ -ecolorable _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable