 Theorem 6. Let \(\theta\) be any formula of \(\LKe\). If \(\theta\) is not atomic, then there is one and only one among (2)–(7) that was the last clause applied to construct \(\theta\). That is, \(\theta\) could not be produced by two different clauses. Moreover, no formula produced by clauses (2)–(7) is atomic.