Erdős Problem 196

Reference: erdosproblems.com/196

theorem Erdos196.erdos_196 : True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

Must every permutation of $\mathbb{N}$, contain a monotone 4-term arithmetic progression?