:: deftheorem defines proper GLCOLO00:def 1 :
for G being _Graph
for f being VColoring of G holds
( f is proper iff for v, w being Vertex of G st v,w are_adjacent holds
f . v <> f . w );