theorem Th85: :: GLCOLO00:85

for G being _Graph
for g being EColoring of G holds
( g is proper iff for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 )