Simplifying the axiomatization for ordered affine geometry via a theorem prover (Q6168184)

\textit{J. von Plato} [Indag. Math., New Ser. 9, No. 4, 549--562 (1998; 0926.51014)] presented an intuitionist axiom system for ordered affine geometry consisting of 22 axioms. One of those axioms, I.7, which actually is the conjunction of four statements, can be simplified, by first noticing that two of the four statements that are part of I.7 are redundant, and then by replacing it with a simpler statement, which is, in essence Theorem 3.10 in von Plato's paper. That the simpler statement that can replace I.7 is Theorem 3.10 was found using an automatic theorem prover called ANDP. The proofs for the equivalence, however, are straightforward.