9Note that, Ahrendt and Giese introduced several types of epsilon semantics. See [Ahre, Def. 4,5]. In [Moln] the substitutional semantics was applied. Now, in TL, the extensional semantics (see [Moln, p.821.] or [Monk, Def. 29.23, p. 481]) will be enough.