:: deftheorem Def21 defines finitely_colorable SCMYCIEL:def 21 :
for G being SimpleGraph holds
( G is finitely_colorable iff ex C being Coloring of G st C is finite );