Translation of intuitive approach:
  For any type S and property Q on S and function-symbol f : S→ℕ, we can prove
    If ∀x∈S ( ∀y∈S ( f(y) < f(x) ⇒ Q(y) ) ⇒ Q(x) ):
      If ¬∀x ∈ S ( Q(x) ):
        ∃x ∈ S ( ¬Q(x) )
        Let c ∈ S such that ¬Q(c)
        f(c) = f(c) ∧ ¬Q(c)
        ∃x ∈ S ( f(x) = f(x) ∧ ¬Q(x) )
        ∃k ∈ ℕ ( ∃x ∈ S ( f(x) = k ∧ ¬Q(x) ) )
        Let m ∈ ℕ such that ∃x ∈ S ( f(x) = m ∧ ¬Q(x) ) ∧ ∀k ∈ ℕ ( ∃x ∈ S ( f(x) = k ∧ ¬Q(x) ) ⇒ k ≥ m ) [well-ordering]
        ∀k ∈ ℕ ( ∃x ∈ S ( f(x) = k ∧ ¬Q(x) ) ⇒ k ≥ m )