for U being Subset of REAL holds { x where x is Element of REAL : x is_local_minimum_of U } is countable