:: deftheorem Def10 defines proper GLCOLO00:def 10 :
for G being _Graph
for t being TColoring of G holds
( t is proper iff ( t _V is proper & t _E is proper & ( for v being Vertex of G holds not (t _V) . v in (t _E) .: (v .edgesInOut()) ) ) );