theorem Th14: :: GLCOLO00:14

for G being _Graph st ex f being VColoring of G st f is proper holds
G is loopless