:: deftheorem Def22 defines chromatic# SCMYCIEL:def 22 :
for G being finitely_colorable SimpleGraph
for b₂ being Nat holds
( b₂ = chromatic# G iff ( ex C being finite Coloring of G st card C = b₂ & ( for C being finite Coloring of G holds b₂ <= card C ) ) );