Another term rewriting based proof of the `non-obvious' theorem