take G = the finite SimpleGraph; :: thesis: G is finitely_colorable
SmallestPartition (Vertices G) is Coloring of G by Th65;
hence G is finitely_colorable ; :: thesis: verum