:: deftheorem Def9 defines TColoring GLCOLO00:def 9 :
for G being _Graph
for b₂ being object holds
( b₂ is TColoring of G iff ex f being VColoring of G ex g being EColoring of G st b₂ = [f,g] );