theorem :: GLCOLO00:28

for G being _Graph st ex c being Cardinal st G is c -vcolorable holds
G is loopless ;