English
If x,y,z are in the ambient space and h encodes a Wbtw relation, then whenever x ∈ s, y and z lie on the same side of s.
Русский
Если x,y,z образуют отношение Wbtw, и x ∈ s, то y и z лежат на одной стороне s.
LaTeX
$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y,z\in P\ ,\forall h:Wbtw\ R x y z,\ hx:\ x \in s\Rightarrow s.WSameSide y z.$$$
Lean4
theorem _root_.Wbtw.wSameSide₂₃ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hx : x ∈ s) :
s.WSameSide y z := by
rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩
exact wSameSide_lineMap_left z hx ht0