theorem Th148: :: GLCOLO00:148

for G being _Graph
for t being TColoring of G holds
( t is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) )