theorem Th30: :: GLCOLO00:30
for G being _Graph holds
( G is edgeless iff G is 1 -vcolorable )