Сильно конструктивная модель без элементарных подмоделей и расширений

Теорема. Пусть $(\mathfrak{M},\nu)$ — сильно конструктивное дискретно упорядоченное множество. Тогда существует обогащение $\mathfrak{M}^{\ast}$ модели одним одноместным предикатом, такое, что $(\mathfrak{M}^{\ast},\nu)$ — сильно конструктивная модель и каждый элемент $a\in |\mathfrak{M}^{\ast}|$ формульно определим в $\mathfrak{M}^{\ast}$.
Отсюда, используя результат автора о том, что существует счетное дискретно упорядоченное множество, не имеющее собственных конструктивных элементарных расширений, получено
Следствие. Существует счетная сильно конструктивная модель сигнатуры $\sigma=\langle <, P^{1}\rangle$, у которой каждый элемент формульно определим и которая не имеет собственных конструктивных элементарных расширений.