English
The strong same-side relation of a point with itself is equivalent to the subspace being nonempty and the point not lying in the subspace.
Русский
Строгое отношение SSameSide точки к самой себе эквивалентно тому, что подпространство непусто и точка не принадлежит ему.
LaTeX
$$$ s.SSameSide x x \iff (s : Set P).Nonempty \land x \notin s $$$
Lean4
theorem sSameSide_self_iff {s : AffineSubspace R P} {x : P} : s.SSameSide x x ↔ (s : Set P).Nonempty ∧ x ∉ s :=
⟨fun ⟨h, hx, _⟩ => ⟨wSameSide_self_iff.1 h, hx⟩, fun ⟨h, hx⟩ => ⟨wSameSide_self_iff.2 h, hx, hx⟩⟩