theorem Th86: :: GLCOLO00:86

for G being _Graph
for g being EColoring of G holds
( g is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 )