注意：本文不是证明，只是一种理解的思路（我不懂怎么证）
如果 \eta \models a \ \mathcal{R} \ b，考察 a，只有两种情况：要么在某步 \eta[i] 中出现过，要么从未没出现过
这里只讨论 a 出现过的情况
\eta 应该是这种情况：
\eta = \{b\}\{b\}\{b\}...\{b\}\{a, b\}...
- 这里只写 a 和 b，并不说原子命题只涉及 a 和 b，而是我只想强调 a 和 b
- 注意，我这里要求 \{a, b\} 是 \eta 中第一次出现 a 的位置
现在，我想改造 \eta 成为 \eta'，使得 \eta' \not \models a \ \mathcal{R} \ b
这里讨论的是 a 必须出现，所以不删 a 只删 b，即
\eta' = \{b\}\{b\}\{\neg b\}...\{b\}\{a, b\}...
现在把关注点落在删掉 b 的那一步，以及该步往前的子串，可以发现 \eta' \models b \ \mathcal{U} \ \neg b
因为 \{a, b\} 是 \eta 第一次出现 a 的位置，所以 \{\neg b\} 之前的 \{b\} 也可以用 \{ \neg a \} 来表示
于是变成了 \eta' \models \neg a \ \mathcal{U} \ \neg b
因为 \eta' \not \models a \ \mathcal{R} \ b，取反就有 \eta' \models \neg(a \ \mathcal{R} \ b)
所以，把 \eta' \models \neg a \ \mathcal{U} \ \neg b 且 \eta' \models \neg(a \ \mathcal{R} \ b) 结合起来看
就有 \neg a \ \mathcal{U} \ \neg b \equiv \neg(a \ \mathcal{R} \ b)
或者 a \ \mathcal{R} \ b \equiv \neg (\neg a \ \mathcal{U} \ \neg b)
再次强调，这不是证明，这只是一种理解思路（我不懂怎么证）