theorem Th146: :: GLCOLO00:146

for G being _Graph
for t being TColoring of G holds
( t is proper iff ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) ) )