let G be SimpleGraph; :: thesis: ( G is finite implies G is finitely_colorable )
assume A1: G is finite ; :: thesis: G is finitely_colorable
SmallestPartition (Vertices G) is Coloring of G by Th65;
hence G is finitely_colorable by A1; :: thesis: verum