theorem Th11: :: GLCOLO00:11

for G being _Graph
for f being VColoring of G holds
( f is proper iff for e, v, w being object st e DJoins v,w,G holds
f . v <> f . w )