let G be SimpleGraph; :: thesis: ( G is finite implies G is finitely_colorable )
assume A: G is finite ; :: thesis: G is finitely_colorable
SmallestPartition (Vertices G) is Coloring of G by Coloring1;
hence G is finitely_colorable by A, Lfc; :: thesis: verum