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