[Nit] Consider using a canonical form of axiom I

[MarcinCiura]

The applications of axiom I base on various permutations of equalities, e.g. (symbolically):
(Proposition I.I) X = Y and X = Z, ∴ Y = Z;
(Proposition I.II) X = Y and Z = X = Y, ∴ Y = Z;
(Proposition I.III) X = Y and Z = X, ∴ Z = Y; etc.
It hurts my OCD so I propose to standardize them on one form, e.g. Y = X and Z = X, ∴ Y = Z.

Below is a diff of my proposal applied to the initial three propositions. If you agree with me, I can make it a PR. Even if you reject the idea, please change \inax[post:I] to \inax[ax:I] in proposition I.I (bug present only in the Russian version) and add \inax[ax:I] to proposition I.II.

-Поскольку $\drawUnitLine{AB} = \drawUnitLine{CA}$ \indef[def:XV];\\
-и $\drawUnitLine{AB} = \drawUnitLine{BC}$ \indef[def:XV];\\
-$\therefore \drawUnitLine{CA} = \drawUnitLine{BC}$ \inax[post:I];\\
+Поскольку $\drawUnitLine{CA} = \drawUnitLine{AB}$ \indef[def:XV];\\
+и $\drawUnitLine{BC} = \drawUnitLine{AB}$ \indef[def:XV];\\
+$\therefore \drawUnitLine{CA} = \drawUnitLine{BC}$ \inax[ax:I];\\

-Поскольку $\drawUnitLine{BE,BD} = \drawUnitLine{DA,AF}$ \indef[def:XV],\\
-и $\drawUnitLine{BD} = \drawUnitLine{DA}$ (постр.),\\
-$\therefore \drawUnitLine{BE} = \drawUnitLine{AF}$ \inax[post:III],\\
-но \indef[def:XV] $\drawUnitLine{BC} = \drawUnitLine{BE} = \drawUnitLine{AF}$;
+Поскольку $\drawUnitLine{DA,AF} = \drawUnitLine{BD,BE}$ \indef[def:XV],\\
+и $\drawUnitLine{DA} = \drawUnitLine{DB}$ (постр.),\\
+$\therefore \drawUnitLine{AF} = \drawUnitLine{BE}$ \inax[post:III],\\
+но $\drawUnitLine{BC} = \drawUnitLine{BE}$ \indef[def:XV];

-$\therefore \drawUnitLine{AF}$ проведенная из данной точки (\pointA) равна данной прямой \drawUnitLine{BC}.
+$\therefore \drawUnitLine{AF}$ проведенная из данной точки (\pointA) равна данной прямой \drawUnitLine{BC} \inax[ax:I].

-Поскольку $\drawUnitLine{AD} = \drawUnitLine{AB}$ \indef[def:XV],\\
+Поскольку $\drawUnitLine{AB} = \drawUnitLine{AD}$ \indef[def:XV],\\
 и $\drawUnitLine{EF} = \drawUnitLine{AD}$ (постр.);

-$\therefore \drawUnitLine{EF} = \drawUnitLine{AB}$ \inax[ax:I];
+$\therefore \drawUnitLine{AB} = \drawUnitLine{EF}$ \inax[ax:I];

[jemmybutton]

That's a good idea, and i agree, that should be done. But ax:I is referenced only five times and is used, i guess, many more times than that in the book, so it would require browsing through all the propositions, and finding all the uses of axiom I by hand (and adding references at the same time, i guess) as you did in prop:I.II.
So for now i fixed obvious bugs: d4a933a#diff-5a8eec69ed8a2717ec1a6d8ee3f6ac94R1185
, d4a933a#diff-5a8eec69ed8a2717ec1a6d8ee3f6ac94R1263 and added the missing reference d4a933a#diff-5a8eec69ed8a2717ec1a6d8ee3f6ac94R1266
(I'm not entirely sure if missing reference is an error that should be fixed in the english version too, or explicitly listing all the references will make proofs look much worse)

In short: yes, i agree with you and will gladly accept your PR, but it may take some time to completely fix this issue