English
For any affine subspace s and points x,y, the relation SS ameSide is symmetric in x and y: s.SSameSide x y iff s.SSameSide y x.
Русский
Для любого аффинного подпространства s и точек x,y отношение SS ameSide симметрично: s.SSameSide x y ⇔ s.SSameSide y x.
LaTeX
$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.SSameSide\; x\; y \iff s.SSameSide\; y\; x$$$
Lean4
theorem sSameSide_comm {s : AffineSubspace R P} {x y : P} : s.SSameSide x y ↔ s.SSameSide y x := by
rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]