Известно, что при помощи моделей легко выводятся некоторые факты, которые трудно установить непосредственно из аксиом. В качестве иллюстрации этого мы получим здесь вывод знаменитой формулы Лобачевского, выражающей функцию угла параллельности П(x) через элементарные функции аргумента x. Рассмотрим модель Кэли-Клейна плоскости Лобачевского в круге Г единичного радиуса на евклидовой плоскости и решим сначала задачу о поиске соотношения, связывающего длины одного и того же отрезка, измеренные в смысле евклидовой геометрии и геометрии Лобачевского.