English
Let s be an affine subspace of P and x, y points of P. If x and y lie on opposite sides of s (in the strong sense), then they also lie on opposite sides of s in the weaker sense.
Русский
Пусть s — аффинное подпространство P и x, y ∈ P. Если x и y лежат по разные стороны s в сильном смысле, то они также лежат по разные стороны s в слабом смысле.
LaTeX
$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.SOppSide\; x\; y\; \Rightarrow\; s.WOppSide\; x\; y$$$
Lean4
theorem wOppSide {s : AffineSubspace R P} {x y : P} (h : s.SOppSide x y) : s.WOppSide x y :=
h.1