Теорема о метризации линейно упорядоченной группы

Пусть

• $a,b,c,d,e,f,g,h,i,j$ - множества,
• $d = \mathrm{\Sigma}(e,f,g)$ - сигнатура,
• $h\in e \ \land \ g(h) = 2_\mathrm{N}$ - символ бинарного отношения,
• $\left|\circ\right| \in f \ \land \ g(\left|\circ\right|) = 1_\mathrm{N}$ - символ унарной операции,
• $i \in f \ \land \ g(i) = 2_\mathrm{N}$ - символ бинарной операции,
• $a = \mathrm{AlgStruct}(b,c,d)$ - алгебраическая структура,
• $a \in \mathrm{LinOrdStruct}(b;h)$ - линейно упорядоченная структура,
• $b \in \mathrm{Group}(b;i)$ - группа,
• $j = \left|\circ\right|_{i_a}^{h_a}$ - операция взятия модуля,

тогда упорядоченная тройка множества $b$, линейно упорядоченной группы $a$ и бинарной операции на множестве $b$ такой, что значение данной бинарной операции от двух любых элементов множества $b$ равно значению операции взятия модуля в линейно упорядоченной группе $a$ от {значения интерпретации символа операции $i$ от первого элемента множества $b$ и некоторой инверсии второго элемента множества $b$ относительно интерпретации символа операции $i$ и некоторого её нейтрального элемента}, является метрическим пространством:

$\begin{cases} \forall a \ \forall b \ \forall c \ \forall d \ \forall e \ \forall f \ \forall g \ \forall h \ \forall i \ \forall j \qquad \begin{cases} d = \mathrm{\Sigma}(e,f,g)\\ h \in e \ \land \ g(h) = 2_\mathrm{N}\\ \left|\circ\right| \in f \ \land \ g(\left|\circ\right|) = 1_\mathrm{N}\\ i \in f \ \land \ g(i) = 2_\mathrm{N}\\ a = \mathrm{AlgStruct}(b,c,d)\\ a \in \mathrm{LinOrdStruct}(b;h)\\ a \in \mathrm{Group}(b;i)\\ j = \left|\circ\right|_{i_a}^{h_a}\\ \end{cases} \Rightarrow \Upsilon(a,\ldots,j)\\ \\ \Upsilon(a,\ldots,j) \ \stackrel{\mathrm{def}}{=} \ \forall k \ \forall l \quad \begin{cases} k = \langle b,a,l \rangle\\ l\in \mathrm{Op}^2(b)\\ \Phi(a,\ldots,l)\\ \end{cases} \Rightarrow k = \mathrm{MetricSpace}(b,a;l)\\ \\ \Phi(a,\ldots,l) \ \stackrel{\mathrm{def}}{=} \ \forall m \ \forall n \quad (\, m\in b \ \land \ n\in b \,) \Rightarrow \Bigl(\, \exists o \ \exists p \quad \bigl(\, o\in \mathrm{Neutral}(i_a) \ \land \ p\in \mathrm{Inversion}_{i_a}^o(n) \,\bigr) \ \land \ l(m,n) = j\bigl(i_a(m,p)\bigr) \,\Bigr) \end{cases}$