English
Let R be a ring with a partial order, and let x, y, z be points of an affine space P over R. The point y is strictly between x and z exactly when y lies on the line segment joining x and z and y is distinct from both endpoints; i.e., y lies on the segment [x, z] and y ≠ x, y ≠ z.
Русский
Пусть R — кольцо с частичным порядком, и пусть x, y, z — точки аффинного пространства P над R. Точка y строго лежит между x и z тогда и только тогда она лежит на отрезке, соединяющем x и z, причём y не равно ни x, ни z; т.е. y ∈ отрезка [x, z] и y ≠ x, y ≠ z.
LaTeX
$$$Sbtw(R,x,y,z) \equiv Wbtw(R,x,y,z) \land y \neq x \land y \neq z$$$
Lean4
/-- The point `y` is strictly between `x` and `z`. -/
def Sbtw (x y z : P) : Prop :=
Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
