English
If x and z are respectively on the same side from y and y on the same side from nothing (non-membership condition), then x and z are on the same side; the relation is transitive given y ∉ s.
Русский
Если x и z лежат по отношению к y на одну и ту же сторону, и y не принадлежит s, то x и z также лежат на одной стороне; отношение транзитивно при условии y ∉ s.
LaTeX
$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y,z\in P\ , s.WSameSide x y\to s.WSameSide y z\to {\text{y} \notin s} \Rightarrow s.WSameSide x z.$$$
Lean4
theorem trans {s : AffineSubspace R P} {x y z : P} (hxy : s.WSameSide x y) (hyz : s.WSameSide y z) (hy : y ∉ s) :
s.WSameSide x z := by
rcases hxy with ⟨p₁, hp₁, p₂, hp₂, hxy⟩
rw [wSameSide_iff_exists_left hp₂, or_iff_right hy] at hyz
rcases hyz with ⟨p₃, hp₃, hyz⟩
refine ⟨p₁, hp₁, p₃, hp₃, hxy.trans hyz ?_⟩
refine fun h => False.elim ?_
rw [vsub_eq_zero_iff_eq] at h
exact hy (h.symm ▸ hp₂)
