HOL-ex.Erdoes_Szekeres